theorem Th15: :: GLIB_016:15
for G1 being _Graph
for G2 being DLGraphComplement of G1 holds
( G1 is Dcomplete iff the_Edges_of G2 = G2 .loops() )