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

then ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v} & the_Edges_of G1 = (the_Edges_of G) \/ (V --> (the_Edges_of G)) ) by Def2;
hence ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by A1, Def3; :: thesis: verum

end;

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

then ( G == G1 & G == G2 ) by Def2, Def3;
then G1 == G2 by GLIB_000:85;
hence ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by GLIB_000:def 34; :: thesis: verum

end;

end;