let G1, G2 be _Graph; :: thesis: for V being set holds
( G2 is removeVertices of G1,V iff G2 is removeVertices of G1,(V /\ (the_Vertices_of G1)) )
let V be set ; :: thesis: ( G2 is removeVertices of G1,V iff G2 is removeVertices of G1,(V /\ (the_Vertices_of G1)) )
(the_Vertices_of G1) \ V = (the_Vertices_of G1) \ (V /\ (the_Vertices_of G1)) by XBOOLE_1:47;
hence ( G2 is removeVertices of G1,V iff G2 is removeVertices of G1,(V /\ (the_Vertices_of G1)) ) ; :: thesis: verum