let G1 be addAdjVertexToAll of G,v,V; G1 is addAdjVertexAll of G,v,V
per cases
( ( V c= the_Vertices_of G & not v in the_Vertices_of G ) or not V c= the_Vertices_of G or v in the_Vertices_of G )
;
suppose A1:
(
V c= the_Vertices_of G & not
v in the_Vertices_of G )
;
G1 is addAdjVertexAll of G,v,Vthen A2:
the_Vertices_of G1 = (the_Vertices_of G) \/ {v}
by Def2;
( ( for
e being
object holds
( not
e Joins v,
v,
G1 & ( for
v1 being
object holds
( ( not
v1 in V implies not
e Joins v1,
v,
G1 ) & ( for
v2 being
object st
v1 <> v &
v2 <> v &
e DJoins v1,
v2,
G1 holds
e DJoins v1,
v2,
G ) ) ) ) ) & ex
E being
set st
(
card V = card E &
E misses the_Edges_of G &
the_Edges_of G1 = (the_Edges_of G) \/ E & ( 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, Lm9;
hence
G1 is
addAdjVertexAll of
G,
v,
V
by A1, A2, Def4;
verum end; end;