let G1 be _Graph; :: thesis: for G2 being G1 -Disomorphic _Graph

for G3 being removeLoops of G1

for G4 being removeLoops of G2 holds G4 is G3 -Disomorphic

let G2 be G1 -Disomorphic _Graph; :: thesis: for G3 being removeLoops of G1

for G4 being removeLoops of G2 holds G4 is G3 -Disomorphic

let G3 be removeLoops of G1; :: thesis: for G4 being removeLoops of G2 holds G4 is G3 -Disomorphic

let G4 be removeLoops of G2; :: thesis: G4 is G3 -Disomorphic

consider F0 being PGraphMapping of G1,G2 such that

A1: F0 is Disomorphism by Def24;

reconsider F0 = F0 as one-to-one PGraphMapping of G1,G2 by A1;

consider F being one-to-one PGraphMapping of G3,G4 such that

F = F0 | G3 and

( F0 is weak_SG-embedding implies F is weak_SG-embedding ) and

( F0 is isomorphism implies F is isomorphism ) and

A2: ( F0 is Disomorphism implies F is Disomorphism ) by Th165;

thus G4 is G3 -Disomorphic by A1, A2; :: thesis: verum

for G3 being removeLoops of G1

for G4 being removeLoops of G2 holds G4 is G3 -Disomorphic

let G2 be G1 -Disomorphic _Graph; :: thesis: for G3 being removeLoops of G1

for G4 being removeLoops of G2 holds G4 is G3 -Disomorphic

let G3 be removeLoops of G1; :: thesis: for G4 being removeLoops of G2 holds G4 is G3 -Disomorphic

let G4 be removeLoops of G2; :: thesis: G4 is G3 -Disomorphic

consider F0 being PGraphMapping of G1,G2 such that

A1: F0 is Disomorphism by Def24;

reconsider F0 = F0 as one-to-one PGraphMapping of G1,G2 by A1;

consider F being one-to-one PGraphMapping of G3,G4 such that

F = F0 | G3 and

( F0 is weak_SG-embedding implies F is weak_SG-embedding ) and

( F0 is isomorphism implies F is isomorphism ) and

A2: ( F0 is Disomorphism implies F is Disomorphism ) by Th165;

thus G4 is G3 -Disomorphic by A1, A2; :: thesis: verum