let G2 be removeLoops of G; :: thesis: G2 is complete

A1: ( the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 = (the_Edges_of G) \ (G .loops()) ) by GLIB_000:53;

A1: ( the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 = (the_Edges_of G) \ (G .loops()) ) by GLIB_000:53;

now :: thesis: for v2, w2 being Vertex of G2 st v2 <> w2 holds

v2,w2 are_adjacent

hence
G2 is complete
by CHORD:def 6; :: thesis: verumv2,w2 are_adjacent

let v2, w2 be Vertex of G2; :: thesis: ( v2 <> w2 implies v2,w2 are_adjacent )

assume A2: v2 <> w2 ; :: thesis: v2,w2 are_adjacent

reconsider v1 = v2, w1 = w2 as Vertex of G by GLIB_000:53;

consider e being object such that

A3: e Joins v1,w1,G by A2, CHORD:def 6, CHORD:def 3;

A4: not e in G .loops() by A2, A3, Th46;

e in the_Edges_of G by A3, GLIB_000:def 13;

then e in the_Edges_of G2 by A1, A4, XBOOLE_0:def 5;

then e Joins v2,w2,G2 by A3, GLIB_000:73;

hence v2,w2 are_adjacent by CHORD:def 3; :: thesis: verum

end;assume A2: v2 <> w2 ; :: thesis: v2,w2 are_adjacent

reconsider v1 = v2, w1 = w2 as Vertex of G by GLIB_000:53;

consider e being object such that

A3: e Joins v1,w1,G by A2, CHORD:def 6, CHORD:def 3;

A4: not e in G .loops() by A2, A3, Th46;

e in the_Edges_of G by A3, GLIB_000:def 13;

then e in the_Edges_of G2 by A1, A4, XBOOLE_0:def 5;

then e Joins v2,w2,G2 by A3, GLIB_000:73;

hence v2,w2 are_adjacent by CHORD:def 3; :: thesis: verum