theorem Th113: :: GLIB_012:113

for G1 being _Graph
for G2 being GraphComplement of G1 holds
( ( G1 is complete implies G2 is edgeless ) & ( G2 is edgeless implies G1 is complete ) & ( the_Edges_of G1 = G1 .loops() implies G2 is complete ) & ( G2 is complete implies the_Edges_of G1 = G1 .loops() ) )