let G1, G2, G3 be _Graph; :: thesis: for G4 being DGraphComplement of G1 st G1 == G2 & G3 == G4 holds
G3 is DGraphComplement of G2
let G4 be DGraphComplement of G1; :: thesis: ( G1 == G2 & G3 == G4 implies G3 is DGraphComplement of G2 )
assume A1: ( G1 == G2 & G3 == G4 ) ; :: thesis: G3 is DGraphComplement of G2
consider G9 being DLGraphComplement of G1 such that
A2: G4 is removeLoops of G9 by Def8;
( G9 is DLGraphComplement of G2 & G3 is removeLoops of G9 ) by A1, A2, Th45, GLIB_009:59;
hence G3 is DGraphComplement of G2 by Def8; :: thesis: verum