let H be DLGraphComplement of G; :: thesis: H is edgeless
H .loops() = {} ;
hence H is edgeless by Th15; :: thesis: verum