let G1 be complete _Graph; :: thesis: for G2 being LGraphComplement of G1 holds the_Edges_of G2 = G2 .loops()
let G2 be LGraphComplement of G1; :: 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 v = (the_Source_of G2) . e;
set w = (the_Target_of G2) . e;
assume e in the_Edges_of G2 ; :: thesis: e in G2 .loops()
then A1: e Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 by GLIB_000:def 13;
(the_Source_of G2) . e = (the_Target_of G2) . e

proof

assume A2: (the_Source_of G2) . e <> (the_Target_of G2) . e ; :: thesis: contradiction
( (the_Source_of G2) . e is Vertex of G2 & (the_Target_of G2) . e is Vertex of G2 ) by A1, GLIB_000:13;
then reconsider v0 = (the_Source_of G2) . e, w0 = (the_Target_of G2) . e as Vertex of G1 by Def7;
ex e0 being object st e0 Joins v0,w0,G1 by A2, CHORD:def 3, CHORD:def 6;
hence contradiction by A1, Th64; :: thesis: verum

end;

hence e in G2 .loops() by A1, GLIB_009:def 2; :: 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