theorem Th57: :: GLIB_012:57

for G1 being _Graph
for G2 being DLGraphComplement of G1 st the_Edges_of G1 = G1 .loops() holds
G2 is complete