theorem :: GLIB_000:123

for G1 being _Graph
for v, e being set
for G2 being removeVertex of G1,v
for G3 being removeEdge of G1,e
for G4 being removeEdge of G2,e holds G4 is removeVertex of G3,v