let G2 be removeDParallelEdges of G; G2 is complete
consider E being RepDEdgeSelection of G such that
A6:
G2 is inducedSubgraph of G, the_Vertices_of G,E
by Def8;
( the_Vertices_of G c= the_Vertices_of G & the_Edges_of G = G .edgesBetween (the_Vertices_of G) )
by GLIB_000:34;
then A7:
( the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 = E )
by A6, 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 b1,b2 are_adjacent )assume A8:
v2 <> w2
;
b1,b2 are_adjacent reconsider v1 =
v2,
w1 =
w2 as
Vertex of
G by A7;
consider e0 being
object such that A9:
e0 Joins v1,
w1,
G
by A8, CHORD:def 6, CHORD:def 3;
per cases
( e0 DJoins v1,w1,G or e0 DJoins w1,v1,G )
by A9, GLIB_000:16;
suppose
e0 DJoins v1,
w1,
G
;
b1,b2 are_adjacent then consider e being
object such that A10:
(
e DJoins v1,
w1,
G &
e in E )
and
for
e9 being
object st
e9 DJoins v1,
w1,
G &
e9 in E holds
e9 = e
by Def6;
e DJoins v2,
w2,
G2
by A7, A10, GLIB_000:73;
then
e Joins v2,
w2,
G2
by GLIB_000:16;
hence
v2,
w2 are_adjacent
by CHORD:def 3;
verum end; suppose
e0 DJoins w1,
v1,
G
;
b1,b2 are_adjacent then consider e being
object such that A11:
(
e DJoins w1,
v1,
G &
e in E )
and
for
e9 being
object st
e9 DJoins w1,
v1,
G &
e9 in E holds
e9 = e
by Def6;
e DJoins w2,
v2,
G2
by A7, A11, GLIB_000:73;
then
e Joins v2,
w2,
G2
by GLIB_000:16;
hence
v2,
w2 are_adjacent
by CHORD:def 3;
verum end; end;
hence
G2 is complete
by CHORD:def 6; verum