let G1 be _Graph; :: thesis: for G2 being LGraphComplement of G1 st the_Edges_of G1 = G1 .loops() holds
G2 is complete
let G2 be LGraphComplement of G1; :: thesis: ( the_Edges_of G1 = G1 .loops() implies G2 is complete )
assume A1: the_Edges_of G1 = G1 .loops() ; :: thesis: G2 is complete

now :: thesis: for v, w being Vertex of G2 st v <> w holds
v,w are_adjacent

let v, w be Vertex of G2; :: thesis: ( v <> w implies v,w are_adjacent )
A2: ( v is Vertex of G1 & w is Vertex of G1 ) by Def7;
assume A3: v <> w ; :: thesis: v,w are_adjacent
for e1 being object holds not e1 Joins v,w,G1

proof

given e1 being object such that A4: e1 Joins v,w,G1 ; :: thesis: contradiction
not e1 in G1 .loops() by A3, A4, GLIB_009:46;
hence contradiction by A1, A4, GLIB_000:def 13; :: thesis: verum

end;

then consider e2 being object such that
A5: e2 Joins v,w,G2 by A2, Def7;
thus v,w are_adjacent by A5, CHORD:def 3; :: thesis: verum

end;

hence G2 is complete by CHORD:def 6; :: thesis: verum