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