let G1 be _Graph; :: thesis: for G2 being DGraphComplement of G1 st the_Edges_of G1 = G1 .loops() holds
G2 is complete
let G2 be DGraphComplement 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 Th80;
assume A3: v <> w ; :: thesis: v,w are_adjacent
for e1 being object holds not e1 DJoins v,w,G1

proof

given e1 being object such that A4: e1 DJoins v,w,G1 ; :: thesis: contradiction
e1 Joins v,w,G1 by A4, GLIB_000:16;
hence contradiction by A1, A3, A4, GLIB_009:46, GLIB_000:def 14; :: thesis: verum

end;

then consider e2 being object such that
A5: e2 DJoins v,w,G2 by A2, A3, Th80;
e2 Joins v,w,G2 by A5, GLIB_000:16;
hence v,w are_adjacent by CHORD:def 3; :: thesis: verum

end;

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