let G1 be _Graph; :: thesis: for G2 being DGraphComplement of G1 holds
( G1 is Dcomplete iff G2 is edgeless )
let G2 be DGraphComplement of G1; :: thesis: ( G1 is Dcomplete iff G2 is edgeless )
consider G9 being DLGraphComplement of G1 such that
A1: G2 is removeLoops of G9 by GLIB_012:def 8;

hereby :: thesis: ( G2 is edgeless implies G1 is Dcomplete )

assume G1 is Dcomplete ; :: thesis: G2 is edgeless
then the_Edges_of G9 = G9 .loops() by Th15;
hence G2 is edgeless by A1; :: thesis: verum

end;

assume G2 is edgeless ; :: thesis: G1 is Dcomplete
then {} = the_Edges_of G2
.= (the_Edges_of G9) \ (G9 .loops()) by A1, GLIB_000:53 ;
then the_Edges_of G9 c= G9 .loops() by XBOOLE_1:37;
hence G1 is Dcomplete by Th15, XBOOLE_0:def 10; :: thesis: verum