theorem Th69: :: GLIB_007:69

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1
for v1, v2 being Vertex of G2 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & W .first() = v1 & W .last() = v2 & not v2 in G2 .reachableFrom v1 holds
v in W .vertices()