let G1 be addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v; :: thesis:
for u1, u2 being Vertex of G1 st u1 <> u2 holds
u1,u2 are_adjacent

proof

let u1, u2 be Vertex of G1; :: thesis:
assume A10: u1 <> u2 ; :: thesis:
set e = the_Edges_of G;
consider w being Vertex of G such that
A11: the_Vertices_of G = {w} by GLIB_000:22;
A12: v = w by A11, TARSKI:def 1;
A13: ( not the_Edges_of G in the_Edges_of G & not the_Vertices_of G in the_Vertices_of G ) ;
then A14: the_Edges_of G Joins {w},w,G1 by A12, A11, Th136;
the_Vertices_of G1 = (the_Vertices_of G) \/ {(the_Vertices_of G)} by A13, Def14
.= {w,{w}} by A11, ENUMSET1:1 ;
then A16: {u1,u2} c= {w,{w}} ;

per cases by ZFMISC_1:22;

suppose A17: u1 = w ; :: thesis:

per cases by A16, ZFMISC_1:22;

suppose u2 = w ; :: thesis:

hence u1,u2 are_adjacent by A10, A17; :: thesis:

end;

suppose u2 = {w} ; :: thesis:

hence u1,u2 are_adjacent by CHORD:def 3, A14, A17; :: thesis:

end;

end;

end;

suppose A18: u1 = {w} ; :: thesis:

per cases by A16, ZFMISC_1:22;

suppose u2 = w ; :: thesis:

hence u1,u2 are_adjacent by A14, A18, CHORD:def 3; :: thesis:

end;

suppose u2 = {w} ; :: thesis:

hence u1,u2 are_adjacent by A10, A18; :: thesis:

end;

end;

end;

end;

end;

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