let G3 be _Graph; :: thesis: for G4 being G3 -Disomorphic _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 -Disomorphic )

let G4 be G3 -Disomorphic _Graph; :: thesis: 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 -Disomorphic )

let v1, v2 be object ; :: thesis: 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 -Disomorphic )

let G1 be addVertex of G3,v1; :: thesis: 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 -Disomorphic )

let G2 be addVertex 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 -Disomorphic )

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

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 -Disomorphic )

let G4 be G3 -Disomorphic _Graph; :: thesis: 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 -Disomorphic )

let v1, v2 be object ; :: thesis: 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 -Disomorphic )

let G1 be addVertex of G3,v1; :: thesis: 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 -Disomorphic )

let G2 be addVertex 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 -Disomorphic )

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

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

end;

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

then
( {v1} \ (the_Vertices_of G3) = {} & {v2} \ (the_Vertices_of G4) = {} )
by ZFMISC_1:60;

then card ({v1} \ (the_Vertices_of G3)) = card ({v2} \ (the_Vertices_of G4)) ;

hence G2 is G1 -Disomorphic by Th147; :: thesis: verum

end;then card ({v1} \ (the_Vertices_of G3)) = card ({v2} \ (the_Vertices_of G4)) ;

hence G2 is G1 -Disomorphic by Th147; :: thesis: verum

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

then
( {v1} \ (the_Vertices_of G3) = {v1} & {v2} \ (the_Vertices_of G4) = {v2} )
by ZFMISC_1:59;

then ( card ({v1} \ (the_Vertices_of G3)) = 1 & card ({v2} \ (the_Vertices_of G4)) = 1 ) by CARD_1:30;

hence G2 is G1 -Disomorphic by Th147; :: thesis: verum

end;then ( card ({v1} \ (the_Vertices_of G3)) = 1 & card ({v2} \ (the_Vertices_of G4)) = 1 ) by CARD_1:30;

hence G2 is G1 -Disomorphic by Th147; :: thesis: verum