let G1 be _Graph; :: thesis: for G2 being G1 -Disomorphic _Graph
for G3 being DLGraphComplement of G1
for G4 being DLGraphComplement of G2 holds G4 is G3 -Disomorphic
let G2 be G1 -Disomorphic _Graph; :: thesis: for G3 being DLGraphComplement of G1
for G4 being DLGraphComplement of G2 holds G4 is G3 -Disomorphic
let G3 be DLGraphComplement of G1; :: thesis: for G4 being DLGraphComplement of G2 holds G4 is G3 -Disomorphic
let G4 be DLGraphComplement of G2; :: thesis: G4 is G3 -Disomorphic
set G5 = the removeDParallelEdges of G1;
set G6 = the removeDParallelEdges of G2;
the removeDParallelEdges of G2 is the removeDParallelEdges of G1 -Disomorphic by GLIB_010:170;
hence G4 is G3 -Disomorphic by Th48; :: thesis: verum