theorem Th75: :: GLIB_012:75
for G1 being complete _Graph
for G2 being LGraphComplement of G1 holds the_Edges_of G2 = G2 .loops()