let G be _Graph; :: thesis: for W being Walk of G
for v being Vertex of G st v in W .vertices() holds
W .vertices() c= G .reachableFrom v
let W be Walk of G; :: thesis: for v being Vertex of G st v in W .vertices() holds
W .vertices() c= G .reachableFrom v
let v be Vertex of G; :: thesis: ( v in W .vertices() implies W .vertices() c= G .reachableFrom v )
assume v in W .vertices() ; :: thesis: W .vertices() c= G .reachableFrom v
then consider m being odd Element of NAT such that
A1: ( m <= len W & W . m = v ) by GLIB_001:88;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in W .vertices() or x in G .reachableFrom v )
assume x in W .vertices() ; :: thesis: x in G .reachableFrom v
then consider n being odd Element of NAT such that
A2: ( n <= len W & W . n = x ) by GLIB_001:88;

now

per cases ( m <= n or m > n ) ;

suppose m <= n ; :: thesis: ex W2 being Walk of G st W2 is_Walk_from v,x

then W .cut m,n is_Walk_from v,x by A1, A2, GLIB_001:38;
hence ex W2 being Walk of G st W2 is_Walk_from v,x ; :: thesis: verum

end;

suppose m > n ; :: thesis: ex W2 being Walk of G st W2 is_Walk_from v,x

then W .cut n,m is_Walk_from x,v by A1, A2, GLIB_001:38;
then (W .cut n,m) .reverse() is_Walk_from v,x by GLIB_001:24;
hence ex W2 being Walk of G st W2 is_Walk_from v,x ; :: thesis: verum

end;

end;

end;

hence x in G .reachableFrom v by Def5; :: thesis: verum