let G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
v is Vertex of G1
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
v is Vertex of G1
let V be set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
v is Vertex of G1
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies v is Vertex of G1 )
assume ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: v is Vertex of G1
then A1: the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by Def4;
v in {v} by TARSKI:def 1;
hence v is Vertex of G1 by A1, XBOOLE_0:def 3; :: thesis: verum