let G1 be _Graph; :: thesis: for G2 being DLGraphComplement of G1 holds
( the_Edges_of G1 = G1 .loops() iff G2 is Dcomplete )
let G2 be DLGraphComplement of G1; :: thesis: ( the_Edges_of G1 = G1 .loops() iff G2 is Dcomplete )

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

assume A1: the_Edges_of G1 = G1 .loops() ; :: thesis: G2 is Dcomplete

now :: thesis: for v2, w2 being Vertex of G2 st v2 <> w2 holds
ex e2 being object st e2 DJoins v2,w2,G2

let v2, w2 be Vertex of G2; :: thesis: ( v2 <> w2 implies ex e2 being object st e2 DJoins v2,w2,G2 )
reconsider v1 = v2, w1 = w2 as Vertex of G1 by GLIB_012:def 6;
assume A2: v2 <> w2 ; :: thesis: ex e2 being object st e2 DJoins v2,w2,G2
for e1 being object holds not e1 DJoins v1,w1,G1

proof

given e1 being object such that A3: e1 DJoins v1,w1,G1 ; :: thesis: contradiction
e1 Joins v1,w1,G1 by A3, GLIB_000:16;
then not e1 in G1 .loops() by A2, GLIB_009:46;
hence contradiction by A1, A3, GLIB_000:def 14; :: thesis: verum

end;

hence ex e2 being object st e2 DJoins v2,w2,G2 by GLIB_012:def 6; :: thesis: verum

end;

hence G2 is Dcomplete ; :: thesis: verum

end;

assume A4: G2 is Dcomplete ; :: thesis: the_Edges_of G1 = G1 .loops()

now :: thesis: for e being object st e in the_Edges_of G1 holds
e in G1 .loops()

let e be object ; :: thesis: ( e in the_Edges_of G1 implies e in G1 .loops() )
set v1 = (the_Source_of G1) . e;
set w1 = (the_Target_of G1) . e;
assume e in the_Edges_of G1 ; :: thesis: e in G1 .loops()
then A5: e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 14;
then e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:16;
then reconsider v1 = (the_Source_of G1) . e, w1 = (the_Target_of G1) . e as Vertex of G1 by GLIB_000:13;
reconsider v2 = v1, w2 = w1 as Vertex of G2 by GLIB_012:def 6;
v1 = w1

proof

assume A6: v1 <> w1 ; :: thesis: contradiction
for e2 being object holds not e2 DJoins v2,w2,G2 by A5, GLIB_012:def 6;
hence contradiction by A4, A6; :: thesis: verum

end;

hence e in G1 .loops() by A5, GLIB_009:45; :: thesis: verum

end;

then the_Edges_of G1 c= G1 .loops() by TARSKI:def 3;
hence the_Edges_of G1 = G1 .loops() by XBOOLE_0:def 10; :: thesis: verum