for G1, G2, G3 being _Graph
for G4 being DLGraphComplement of G1 st G1 == G2 & G3 == G4 holds
G3 is DLGraphComplement of G2