for G1 being _Graph
for G2 being reverseEdgeDirections of G1
for G3 being DLGraphComplement of G1
for G4 being reverseEdgeDirections of G3 holds G4 is DLGraphComplement of G2