theorem :: GLIB_000:165

for G1, G2 being _Graph
for V being set holds
( G2 is removeVertices of G1,V iff G2 is removeVertices of G1,(V /\ (the_Vertices_of G1)) )