let G1 be _Graph; :: thesis: for G2 being G1 -isomorphic _Graph
for G3 being LGraphComplement of G1
for G4 being LGraphComplement of G2 holds G4 is G3 -isomorphic
let G2 be G1 -isomorphic _Graph; :: thesis: for G3 being LGraphComplement of G1
for G4 being LGraphComplement of G2 holds G4 is G3 -isomorphic
let G3 be LGraphComplement of G1; :: thesis: for G4 being LGraphComplement of G2 holds G4 is G3 -isomorphic
let G4 be LGraphComplement of G2; :: thesis: G4 is G3 -isomorphic
set G5 = the removeParallelEdges of G1;
set G6 = the removeParallelEdges of G2;
the removeParallelEdges of G2 is the removeParallelEdges of G1 -isomorphic by GLIB_010:168;
hence G4 is G3 -isomorphic by Th66; :: thesis: verum