let G3 be _Graph; :: thesis: for G4 being G3 -Disomorphic _Graph
for V1, V2 being set
for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2 st card (V1 \ ()) = card (V2 \ ()) holds
G2 is G1 -Disomorphic

let G4 be G3 -Disomorphic _Graph; :: thesis: for V1, V2 being set
for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2 st card (V1 \ ()) = card (V2 \ ()) holds
G2 is G1 -Disomorphic

let V1, V2 be set ; :: thesis: for G1 being addVertices of G3,V1
for G2 being addVertices of G4,V2 st card (V1 \ ()) = card (V2 \ ()) holds
G2 is G1 -Disomorphic

let G1 be addVertices of G3,V1; :: thesis: for G2 being addVertices of G4,V2 st card (V1 \ ()) = card (V2 \ ()) holds
G2 is G1 -Disomorphic

let G2 be addVertices of G4,V2; :: thesis: ( card (V1 \ ()) = card (V2 \ ()) implies G2 is G1 -Disomorphic )
assume card (V1 \ ()) = card (V2 \ ()) ; :: thesis: G2 is G1 -Disomorphic
then consider f being Function such that
A1: ( f is one-to-one & dom f = V1 \ () & rng f = V2 \ () ) by ;
reconsider f = f as one-to-one Function by A1;
consider F0 being PGraphMapping of G3,G4 such that
A2: F0 is Disomorphism by Def24;
consider F being PGraphMapping of G1,G2 such that
F = [((F0 _V) +* f),(F0 _E)] and
( F0 is weak_SG-embedding implies F is weak_SG-embedding ) and
( F0 is strong_SG-embedding implies F is strong_SG-embedding ) and
( F0 is isomorphism implies F is isomorphism ) and
A3: ( F0 is Disomorphism implies F is Disomorphism ) by ;
thus G2 is G1 -Disomorphic by A2, A3; :: thesis: verum