let G be _Graph; :: thesis: for v being object
for V being set
for G1, G2 being addAdjVertexToAll of G,v,V holds G1 == G2
let v be object ; :: thesis: for V being set
for G1, G2 being addAdjVertexToAll of G,v,V holds G1 == G2
let V be set ; :: thesis: for G1, G2 being addAdjVertexToAll of G,v,V holds G1 == G2
let G1, G2 be addAdjVertexToAll of G,v,V; :: thesis: G1 == G2

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 ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: G1 == G2

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) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of G1 = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) & 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) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of G2 = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) ) by Def2;
hence G1 == G2 by GLIB_000:def 34; :: thesis: verum

end;

suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: G1 == G2

then ( G == G1 & G == G2 ) by Def2;
hence G1 == G2 by GLIB_000:85; :: thesis: verum

end;

end;