theorem Th22: :: GLIB_007:22

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v being set
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})