for G1 being non-multi _Graph
for G2 being GraphFromSymRel of (the_Vertices_of G1),(VertexAdjSymRel G1) holds G2 is G1 -isomorphic