theorem Th74: :: GLIB_012:74
for G1 being _Graph
for G2 being LGraphComplement of G1 st the_Edges_of G1 = G1 .loops() holds
G2 is complete