let G1 be addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G; 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 A1:
u1 <> u2
;
u1,u2 are_adjacent
set e =
the_Edges_of G;
consider w being
Vertex of
G such that A2:
the_Vertices_of G = {w}
by GLIB_000:22;
A3:
v = w
by A2, TARSKI:def 1;
A4:
( not
the_Edges_of G in the_Edges_of G & not
the_Vertices_of G in the_Vertices_of G )
;
then A5:
the_Edges_of G Joins w,
{w},
G1
by A2, A3, Th135;
the_Vertices_of G1 =
(the_Vertices_of G) \/ {(the_Vertices_of G)}
by A4, Def13
.=
{w,{w}}
by A2, ENUMSET1:1
;
then A7:
{u1,u2} c= {w,{w}}
;
end;
hence
G1 is complete
by CHORD:def 6; verum