let G2 be removeParallelEdges of G; :: thesis: G2 is complete
consider E being RepEdgeSelection of G such that
A1: G2 is inducedSubgraph of G, the_Vertices_of G,E by Def7;
( the_Vertices_of G c= the_Vertices_of G & the_Edges_of G = G .edgesBetween (the_Vertices_of G) ) by GLIB_000:34;
then A2: ( the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 = E ) by A1, GLIB_000:def 37;

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

let v2, w2 be Vertex of G2; :: thesis: ( v2 <> w2 implies v2,w2 are_adjacent )
assume A3: v2 <> w2 ; :: thesis: v2,w2 are_adjacent
reconsider v1 = v2, w1 = w2 as Vertex of G by A2;
consider e0 being object such that
A4: e0 Joins v1,w1,G by A3, CHORD:def 6, CHORD:def 3;
consider e being object such that
A5: ( e Joins v1,w1,G & e in E ) and
for e9 being object st e9 Joins v1,w1,G & e9 in E holds
e9 = e by A4, Def5;
e Joins v2,w2,G2 by A2, A5, GLIB_000:73;
hence v2,w2 are_adjacent by CHORD:def 3; :: thesis: verum

end;

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