let G1 be non-multi _Graph; :: thesis: for G2 being GraphFromSymRel of (the_Vertices_of G1),(VertexAdjSymRel G1) holds G2 is G1 -isomorphic
let G2 be GraphFromSymRel of (the_Vertices_of G1),(VertexAdjSymRel G1); :: thesis: G2 is G1 -isomorphic
consider F being PGraphMapping of G1,G2 such that
A1: F is isomorphism and
( 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)] ) ) ) by Th106;
thus G2 is G1 -isomorphic by A1, GLIB_010:def 23; :: thesis: verum