let G2 be removeDParallelEdges of G; :: thesis: 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;

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 :: 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 b_{1},b_{2} are_adjacent )

assume A8: v2 <> w2 ; :: thesis: b_{1},b_{2} 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;

end;assume A8: v2 <> w2 ; :: thesis: b

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;

end;

suppose
e0 DJoins v1,w1,G
; :: thesis: b_{1},b_{2} 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; :: thesis: verum

end;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; :: thesis: verum

suppose
e0 DJoins w1,v1,G
; :: thesis: b_{1},b_{2} 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; :: thesis: verum

end;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; :: thesis: verum