let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be set ; :: thesis:
let G1 be addAdjVertexAll of G2,v,V; :: thesis:
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis:

hereby :: thesis:

assume A2: G1 is complete ; :: thesis:
for u, v being Vertex of G2 st u <> v holds
u,v are_adjacent

let u2, v2 be Vertex of G2; :: thesis:
reconsider u1 = u2, v1 = v2 as Vertex of G1 by GLIB_006:68;
assume u2 <> v2 ; :: thesis:
then u1 <> v1 ;
then u1,v1 are_adjacent by A2, CHORD:def 6;
then consider e being object such that
A3: e Joins u1,v1,G1 by CHORD:def 3;
( u2 <> v & v2 <> v ) by A1;
then e Joins u2,v2,G2 by A1, A3, Th49;
hence u2,v2 are_adjacent by CHORD:def 3; :: thesis:

end;

hence G2 is complete by CHORD:def 6; :: thesis:
for x being object st x in the_Vertices_of G2 holds
x in V

let x be object ; :: thesis:
assume x in the_Vertices_of G2 ; :: thesis:
then reconsider v2 = x as Vertex of G2 ;
reconsider v1 = v2 as Vertex of G1 by GLIB_006:68;
reconsider v0 = v as Vertex of G1 by A1, Th50;
v1 <> v by A1;
then v1,v0 are_adjacent by A2, CHORD:def 6;
then consider e being object such that
A4: e Joins v1,v,G1 by CHORD:def 3;
thus x in V by A1, A4, Def4; :: thesis:

end;

then the_Vertices_of G2 c= V by TARSKI:def 3;
hence V = the_Vertices_of G2 by A1, XBOOLE_0:def 10; :: thesis:

end;

assume that
A5: G2 is complete and
A6: V = the_Vertices_of G2 ; :: thesis:
for u, v being Vertex of G1 st u <> v holds
u,v are_adjacent

let u1, v1 be Vertex of G1; :: thesis:
assume A7: u1 <> v1 ; :: thesis:
consider E being set such that
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E ) and
A8: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by A1, Def4;
A9: the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by A1, Def4;

suppose A10: u1 = v ; :: thesis:

then v1 <> v by A7;
then not v1 in {v} by TARSKI:def 1;
then v1 in the_Vertices_of G2 by A9, XBOOLE_0:def 3;
then consider e1 being object such that
A11: ( e1 in E & e1 Joins v1,v,G1 ) and
for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 by A6, A8;
e1 Joins u1,v1,G1 by A10, A11, GLIB_000:14;
hence u1,v1 are_adjacent by CHORD:def 3; :: thesis:

end;

suppose A12: v1 = v ; :: thesis:

then u1 <> v by A7;
then not u1 in {v} by TARSKI:def 1;
then u1 in the_Vertices_of G2 by A9, XBOOLE_0:def 3;
then consider e1 being object such that
A13: ( e1 in E & e1 Joins u1,v,G1 ) and
for e2 being object st e2 Joins u1,v,G1 holds
e1 = e2 by A6, A8;
e1 Joins u1,v1,G1 by A12, A13;
hence u1,v1 are_adjacent by CHORD:def 3; :: thesis:

end;

suppose ( u1 <> v & v1 <> v ) ; :: thesis:

then ( not u1 in {v} & not v1 in {v} ) by TARSKI:def 1;
then reconsider u2 = u1, v2 = v1 as Vertex of G2 by A9, XBOOLE_0:def 3;
u2,v2 are_adjacent by A5, A7, CHORD:def 6;
then consider e being object such that
A14: e Joins u2,v2,G2 by CHORD:def 3;
e Joins u1,v1,G1 by A14, GLIB_006:70;
hence u1,v1 are_adjacent by CHORD:def 3; :: thesis:

end;

end;

end;

hence G1 is complete by CHORD:def 6; :: thesis: