let G, G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexFromAll of G,v,V st G1 == G2 holds
G2 is addAdjVertexFromAll of G,v,V
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexFromAll of G,v,V st G1 == G2 holds
G2 is addAdjVertexFromAll of G,v,V
let V be set ; :: thesis: for G1 being addAdjVertexFromAll of G,v,V st G1 == G2 holds
G2 is addAdjVertexFromAll of G,v,V
let G1 be addAdjVertexFromAll of G,v,V; :: thesis: ( G1 == G2 implies G2 is addAdjVertexFromAll of G,v,V )
assume A1: G1 == G2 ; :: thesis: G2 is addAdjVertexFromAll 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 A2: ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: G2 is addAdjVertexFromAll of G,v,V

then ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v} & the_Edges_of G1 = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of G1 = (the_Source_of G) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of G1 = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) ) by Def3;
then A3: ( the_Vertices_of G2 = (the_Vertices_of G) \/ {v} & the_Edges_of G2 = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of G2 = (the_Source_of G) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of G2 = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) ) by A1, GLIB_000:def 34;
G2 is Supergraph of G1 by A1, GLIB_006:59;
then G2 is Supergraph of G by GLIB_006:62;
hence G2 is addAdjVertexFromAll of G,v,V by A2, A3, Def3; :: thesis: verum

end;

suppose A4: ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: G2 is addAdjVertexFromAll of G,v,V

then G == G1 by Def3;
then A5: G == G2 by A1, GLIB_000:85;
then G2 is Supergraph of G by GLIB_006:59;
hence G2 is addAdjVertexFromAll of G,v,V by A4, A5, Def3; :: thesis: verum

end;

end;