let G3 be _Graph; :: thesis: for G4 being G3 -isomorphic _Graph

for v1, v2 being object

for G1 being addAdjVertexAll of G3,v1

for G2 being addAdjVertexAll of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

let G4 be G3 -isomorphic _Graph; :: thesis: for v1, v2 being object

for G1 being addAdjVertexAll of G3,v1

for G2 being addAdjVertexAll of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

let v1, v2 be object ; :: thesis: for G1 being addAdjVertexAll of G3,v1

for G2 being addAdjVertexAll of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

let G1 be addAdjVertexAll of G3,v1; :: thesis: for G2 being addAdjVertexAll of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

let G2 be addAdjVertexAll of G4,v2; :: thesis: not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

assume ( v1 in the_Vertices_of G3 iff v2 in the_Vertices_of G4 ) ; :: thesis: G2 is G1 -isomorphic

for v1, v2 being object

for G1 being addAdjVertexAll of G3,v1

for G2 being addAdjVertexAll of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

let G4 be G3 -isomorphic _Graph; :: thesis: for v1, v2 being object

for G1 being addAdjVertexAll of G3,v1

for G2 being addAdjVertexAll of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

let v1, v2 be object ; :: thesis: for G1 being addAdjVertexAll of G3,v1

for G2 being addAdjVertexAll of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

let G1 be addAdjVertexAll of G3,v1; :: thesis: for G2 being addAdjVertexAll of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

let G2 be addAdjVertexAll of G4,v2; :: thesis: not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

assume ( v1 in the_Vertices_of G3 iff v2 in the_Vertices_of G4 ) ; :: thesis: G2 is G1 -isomorphic

per cases then
( ( not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 ) or ( v1 in the_Vertices_of G3 & v2 in the_Vertices_of G4 ) )
;

end;

suppose A1:
( not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 )
; :: thesis: G2 is G1 -isomorphic

consider F0 being PGraphMapping of G3,G4 such that

A2: F0 is isomorphism by Def23;

A3: (F0 _V) | (the_Vertices_of G3) is one-to-one by A2;

A4: dom ((F0 _V) | (the_Vertices_of G3)) = the_Vertices_of G3 by A2, Def11;

rng ((F0 _V) | (the_Vertices_of G3)) = the_Vertices_of G4 by A2, Def12;

then consider F being PGraphMapping of G1,G2 such that

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E ) 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 weak_SG-embedding implies F is weak_SG-embedding ) and

A5: ( F0 is isomorphism implies F is isomorphism ) by A1, A3, A4, Th162;

thus G2 is G1 -isomorphic by A2, A5; :: thesis: verum

end;A2: F0 is isomorphism by Def23;

A3: (F0 _V) | (the_Vertices_of G3) is one-to-one by A2;

A4: dom ((F0 _V) | (the_Vertices_of G3)) = the_Vertices_of G3 by A2, Def11;

rng ((F0 _V) | (the_Vertices_of G3)) = the_Vertices_of G4 by A2, Def12;

then consider F being PGraphMapping of G1,G2 such that

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E ) 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 weak_SG-embedding implies F is weak_SG-embedding ) and

A5: ( F0 is isomorphism implies F is isomorphism ) by A1, A3, A4, Th162;

thus G2 is G1 -isomorphic by A2, A5; :: thesis: verum

suppose
( v1 in the_Vertices_of G3 & v2 in the_Vertices_of G4 )
; :: thesis: G2 is G1 -isomorphic

then
( G1 == G3 & G2 == G4 )
by GLIB_007:def 4;

then ( G1 is reverseEdgeDirections of G3, {} & G2 is reverseEdgeDirections of G4, {} ) by GLIB_009:42;

hence G2 is G1 -isomorphic by Th143; :: thesis: verum

end;then ( G1 is reverseEdgeDirections of G3, {} & G2 is reverseEdgeDirections of G4, {} ) by GLIB_009:42;

hence G2 is G1 -isomorphic by Th143; :: thesis: verum