let G1 be addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v; 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;
( u1 <> u2 implies u1,u2 are_adjacent )
assume A10:
u1 <> u2
;
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}}
;
end;
hence
G1 is complete
by CHORD:def 6; verum