theorem Th90: :: GLIB_012:90
for G1 being _Graph
for G2 being DGraphComplement of G1 holds G1 .order() = G2 .order() by Th80;