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

hereby :: thesis: ( G2 is Dcomplete implies the_Edges_of G1 = G1 .loops() )

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

end;

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