theorem :: GLIB_000:124

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