theorem Th25: :: GLIB_008:25

for G1 being _Graph
for v0, v1 being Vertex of G1
for G2 being removeVertex of G1,v0
for v2 being Vertex of G2 st v0 is endvertex & v1 = v2 & v1 in G1 .reachableFrom v0 holds
G2 .reachableFrom v2 = (G1 .reachableFrom v1) \ {v0}