for G1 being non-multi _Graph
for G2 being GraphFromSymRel of (the_Vertices_of G1),(VertexAdjSymRel G1) ex F being PGraphMapping of G1,G2 st
( F is isomorphism & F _V = id (the_Vertices_of G1) & ( for e being object holds
( not e in the_Edges_of G1 or (F _E) . e = [((the_Source_of G1) . e),((the_Target_of G1) . e)] or (F _E) . e = [((the_Target_of G1) . e),((the_Source_of G1) . e)] ) ) )