let G3 be _Graph; for G4 being G3 -isomorphic _Graph
for v1, v2 being object
for G1 being addVertex of G3,v1
for G2 being addVertex 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; for v1, v2 being object
for G1 being addVertex of G3,v1
for G2 being addVertex 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 ; for G1 being addVertex of G3,v1
for G2 being addVertex 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 addVertex of G3,v1; for G2 being addVertex 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 addVertex of G4,v2; 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 )
; G2 is G1 -isomorphic