let G2 be removeParallelEdges of G; 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 for v2, w2 being Vertex of G2 st v2 <> w2 holds
v2,w2 are_adjacent let v2,
w2 be
Vertex of
G2;
( v2 <> w2 implies v2,w2 are_adjacent )assume A3:
v2 <> w2
;
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;
verum end;
hence
G2 is complete
by CHORD:def 6; verum