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

proof

let u1, u2 be Vertex of G1; :: thesis: ( u1 <> u2 implies u1,u2 are_adjacent )
assume A10: u1 <> u2 ; :: thesis: u1,u2 are_adjacent
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 then ( u1 = w or u1 = {w} ) by ZFMISC_1:22;

suppose A17: u1 = w ; :: thesis: u1,u2 are_adjacent

per cases ( u2 = w or u2 = {w} ) by A16, ZFMISC_1:22;

suppose u2 = w ; :: thesis: u1,u2 are_adjacent

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

end;

suppose u2 = {w} ; :: thesis: u1,u2 are_adjacent

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

end;

end;

end;

suppose A18: u1 = {w} ; :: thesis: u1,u2 are_adjacent

per cases ( u2 = w or u2 = {w} ) by A16, ZFMISC_1:22;

suppose u2 = w ; :: thesis: u1,u2 are_adjacent

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

end;

suppose u2 = {w} ; :: thesis: u1,u2 are_adjacent

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

end;

end;

end;

end;

end;

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