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;

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,xend;

hence
x in G .reachableFrom v
by Def5; :: thesis: verumper cases
( m <= n or m > n )
;

end;

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;hence ex W2 being Walk of G st W2 is_Walk_from v,x ; :: thesis: verum

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;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