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 and
A2: W . m = v by GLIB_001:87;
let x be object ; :: 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
A3: n <= len W and
A4: W . n = x by GLIB_001:87;

now :: thesis: ex W2 being Walk of G st W2 is_Walk_from v,x

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 A2, A3, A4, GLIB_001:37;
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, A4, GLIB_001:37;
then (W .cut (n,m)) .reverse() is_Walk_from v,x by GLIB_001:23;
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