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