let H be DLGraphComplement of G; :: thesis: H is Dcomplete
( the_Edges_of G = {} & G .loops() = {} ) ;
hence H is Dcomplete by Th14; :: thesis: verum