let G3 be _Graph; :: thesis: for V, E being set
for G4 being reverseEdgeDirections of G3,E
for G1 being addLoops of G3,V
for G2 being addLoops of G4,V holds G2 is G1 -isomorphic
let V, E be set ; :: thesis: for G4 being reverseEdgeDirections of G3,E
for G1 being addLoops of G3,V
for G2 being addLoops of G4,V holds G2 is G1 -isomorphic
let G4 be reverseEdgeDirections of G3,E; :: thesis: for G1 being addLoops of G3,V
for G2 being addLoops of G4,V holds G2 is G1 -isomorphic
let G1 be addLoops of G3,V; :: thesis: for G2 being addLoops of G4,V holds G2 is G1 -isomorphic
let G2 be addLoops of G4,V; :: thesis: G2 is G1 -isomorphic

per cases ( V c= the_Vertices_of G3 or not V c= the_Vertices_of G3 ) ;

suppose A1: V c= the_Vertices_of G3 ; :: thesis: G2 is G1 -isomorphic

consider F0 being PGraphMapping of G3,G4 such that
A2: ( F0 = id G3 & F0 is isomorphism ) by GLIBPRE0:77;
A3: (F0 _V) | V is one-to-one by A2, FUNCT_1:52;
A4: dom ((F0 _V) | V) = (dom (F0 _V)) /\ V by RELAT_1:61
.= V by A1, A2, XBOOLE_1:28 ;
A5: rng ((F0 _V) | V) = ((id G3) _V) .: V by A2, RELAT_1:115
.= V by A1, FUNCT_1:92 ;
consider F being PGraphMapping of G1,G2 such that
( F _V = F0 _V & (F _E) | (dom (F0 _E)) = F0 _E ) and
( not F0 is empty implies not F is empty ) and
( F0 is total implies F is total ) and
( F0 is onto implies F is onto ) and
( F0 is one-to-one implies F is one-to-one ) and
( F0 is directed implies F is directed ) and
( F0 is weak_SG-embedding implies F is weak_SG-embedding ) and
A6: ( F0 is isomorphism implies F is isomorphism ) and
( F0 is Disomorphism implies F is Disomorphism ) by A1, A3, A4, A5, Th29;
thus G2 is G1 -isomorphic by A2, A6, GLIB_010:def 23; :: thesis: verum

end;

suppose not V c= the_Vertices_of G3 ; :: thesis: G2 is G1 -isomorphic

then ( G1 == G3 & not V c= the_Vertices_of G4 ) by Def5, GLIB_007:4;
then A7: ( G1 == G3 & G2 == G4 ) by Def5;
then G2 is reverseEdgeDirections of G3,E by GLIB_007:2;
then G3 is reverseEdgeDirections of G2,E by GLIB_007:3;
then G1 is reverseEdgeDirections of G2,E by A7, GLIB_007:2;
then G2 is reverseEdgeDirections of G1,E by GLIB_007:3;
hence G2 is G1 -isomorphic by GLIBPRE0:78; :: thesis: verum

end;

end;