for G1 being non _trivial _Graph
for v0, v1 being Vertex of G1
for G2 being removeVertex of G1,v0
for v2 being Vertex of G2 st v1 = v2 & not v1 in G1 .reachableFrom v0 holds
G2 .reachableFrom v2 = G1 .reachableFrom v1