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

for G3 being DSimpleGraph of G1

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

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

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

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

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

set G5 = the removeLoops of G1;

set G6 = the removeLoops of G2;

A1: the removeLoops of G2 is the removeLoops of G1 -Disomorphic by Th167;

( G3 is removeDParallelEdges of the removeLoops of G1 & G4 is removeDParallelEdges of the removeLoops of G2 ) by GLIB_009:122;

hence G4 is G3 -Disomorphic by A1, Th170; :: thesis: verum

for G3 being DSimpleGraph of G1

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

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

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

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

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

set G5 = the removeLoops of G1;

set G6 = the removeLoops of G2;

A1: the removeLoops of G2 is the removeLoops of G1 -Disomorphic by Th167;

( G3 is removeDParallelEdges of the removeLoops of G1 & G4 is removeDParallelEdges of the removeLoops of G2 ) by GLIB_009:122;

hence G4 is G3 -Disomorphic by A1, Th170; :: thesis: verum