theorem :: GLIB_002:13

for G being _Graph
for v being Vertex of G
for W being Walk of G st v in W .vertices() holds
W .vertices() c= G .reachableFrom v by Lm4;