Description: Define the class of all undirected simple graphs (without loops). An
undirected simple graph is a special undirected simple pseudograph (see
usgruspgr ), consisting of a set v (of "vertices") and an
injective (one-to-one) function e (representing (indexed) "edges")
into subsets of v of cardinality two, representing the two vertices
incident to the edge. In contrast to an undirected simple pseudograph,
an undirected simple graph has no loops (edges connecting a vertex with
itself). (Contributed by Alexander van der Vekens, 10-Aug-2017)(Revised by AV, 13-Oct-2020)