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

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

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

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

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

proof

assume A3: v1 <> w1 ; :: thesis: contradiction
for e2 being object holds not e2 DJoins v2,w2,G1 by A2, GLIB_012:def 6;
hence contradiction by A1, A3; :: thesis: verum

end;

hence e in G2 .loops() by A2, GLIB_009:45; :: thesis: verum

end;

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

end;

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

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

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

proof

given e1 being object such that A6: e1 DJoins v1,w1,G2 ; :: thesis: contradiction
e1 Joins v1,w1,G2 by A6, GLIB_000:16;
then not e1 in G2 .loops() by A5, GLIB_009:46;
hence contradiction by A4, A6, GLIB_000:def 14; :: thesis: verum

end;

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

end;

hence G1 is Dcomplete ; :: thesis: verum