let G1 be addAdjVertexFromAll of G,v,V; :: thesis: 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 A4: ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: G1 is addAdjVertexAll of G,v,V

then A5: the_Vertices_of G1 = (the_Vertices_of G) \/ {v} by Def3;
( ( 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 A4, Lm10;
hence G1 is addAdjVertexAll of G,v,V by A4, A5, Def4; :: thesis: verum

end;

suppose A6: ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: G1 is addAdjVertexAll of G,v,V

then G1 == G by Def3;
hence G1 is addAdjVertexAll of G,v,V by A6, Def4; :: thesis: verum

end;

end;