theorem Th16: :: GLIB_016:16
for G1 being _Graph
for G2 being DGraphComplement of G1 holds
( the_Edges_of G1 = G1 .loops() iff G2 is Dcomplete )