let G2 be LGraphComplement of G; :: thesis: G2 is edgeless
the_Edges_of G2 = G2 .loops() by Th75
.= {} ;
hence G2 is edgeless ; :: thesis: verum