let G be _Graph; :: thesis: for v being object
for V being set
for G1, G2 being addAdjVertexAll of G,v,V holds
( the_Vertices_of G1 = the_Vertices_of G2 & ( for v1 being Vertex of G1 holds v1 is Vertex of G2 ) )
let v be object ; :: thesis: for V being set
for G1, G2 being addAdjVertexAll of G,v,V holds
( the_Vertices_of G1 = the_Vertices_of G2 & ( for v1 being Vertex of G1 holds v1 is Vertex of G2 ) )
let V be set ; :: thesis: for G1, G2 being addAdjVertexAll of G,v,V holds
( the_Vertices_of G1 = the_Vertices_of G2 & ( for v1 being Vertex of G1 holds v1 is Vertex of G2 ) )
let G1, G2 be addAdjVertexAll of G,v,V; :: thesis: ( the_Vertices_of G1 = the_Vertices_of G2 & ( for v1 being Vertex of G1 holds v1 is Vertex of G2 ) )
thus the_Vertices_of G1 = the_Vertices_of G2 :: thesis: for v1 being Vertex of G1 holds v1 is Vertex of G2

proof

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: the_Vertices_of G1 = the_Vertices_of G2

then ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v} & the_Vertices_of G2 = (the_Vertices_of G) \/ {v} ) by Def4;
hence the_Vertices_of G1 = the_Vertices_of G2 ; :: 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

then ( G1 == G & G2 == G ) by Def4;
then G1 == G2 by GLIB_000:85;
hence the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:def 34; :: thesis: verum

end;

end;

end;

hence for v1 being Vertex of G1 holds v1 is Vertex of G2 ; :: thesis: verum