theorem :: GLIB_012:89
for G1 being Dsimple _Graph
for G2 being DGraphComplement of G1 holds G1 is DGraphComplement of G2