theorem :: GLIB_000:50

for G1 being _finite _Graph
for V being Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V st V <> the_Vertices_of G1 holds
( (G2 .order()) + (card V) = G1 .order() & (G2 .size()) + (card (G1 .edgesInOut V)) = G1 .size() )