alternative definition of a multigraph

Many authors tried to formalize the notation of a graph. This problem is relatively simple if we allow at most $1$ edge between vertices. But for multigraphs, i.e. graphs with many edges (possibly infinitely many) between vertices this tends to be problematic formally. We wish to give an alternative definition, which uses so called symmetric power (http://planetmath.org/SymmetricPower).

Definition. A multigraph or non-oriented graph is a triple

$$G=(V,E,\tau )$$

where $V$ is a nonempty set whose elements are called vertices, $E$ is a set whose elements are called edges and

$$\tau :E\to V_{sym}^2$$

is a function which takes every edge to a pair of vertices called ends of this edge. On the right side we have a symmetric power (http://planetmath.org/SymmetricPower) of $V$ to ensure that the order of ends is not important.

This definition allows loops and even infinite number of edges between two vertices and is one of the most general and formal.