let G2 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V
for v being object st v in V holds
v is Vertex of G1
let V be set ; :: thesis: for G1 being addVertices of G2,V
for v being object st v in V holds
v is Vertex of G1
let G1 be addVertices of G2,V; :: thesis: for v being object st v in V holds
v is Vertex of G1
let v be object ; :: thesis: ( v in V implies v is Vertex of G1 )
assume v in V ; :: thesis: v is Vertex of G1
then v in V \/ (the_Vertices_of G2) by XBOOLE_0:def 3;
hence v is Vertex of G1 by Def10; :: thesis: verum