let G be _Graph; :: thesis: for W being Walk of G

for x, y being set st x in W .vertices() & y in W .vertices() holds

ex W9 being Walk of G st W9 is_Walk_from x,y

let W be Walk of G; :: thesis: for x, y being set st x in W .vertices() & y in W .vertices() holds

ex W9 being Walk of G st W9 is_Walk_from x,y

let x, y be set ; :: thesis: ( x in W .vertices() & y in W .vertices() implies ex W9 being Walk of G st W9 is_Walk_from x,y )

assume that

A1: x in W .vertices() and

A2: y in W .vertices() ; :: thesis: ex W9 being Walk of G st W9 is_Walk_from x,y

consider m being odd Element of NAT such that

A3: m <= len W and

A4: W . m = x by A1, Lm45;

consider n being odd Element of NAT such that

A5: n <= len W and

A6: W . n = y by A2, Lm45;

for x, y being set st x in W .vertices() & y in W .vertices() holds

ex W9 being Walk of G st W9 is_Walk_from x,y

let W be Walk of G; :: thesis: for x, y being set st x in W .vertices() & y in W .vertices() holds

ex W9 being Walk of G st W9 is_Walk_from x,y

let x, y be set ; :: thesis: ( x in W .vertices() & y in W .vertices() implies ex W9 being Walk of G st W9 is_Walk_from x,y )

assume that

A1: x in W .vertices() and

A2: y in W .vertices() ; :: thesis: ex W9 being Walk of G st W9 is_Walk_from x,y

consider m being odd Element of NAT such that

A3: m <= len W and

A4: W . m = x by A1, Lm45;

consider n being odd Element of NAT such that

A5: n <= len W and

A6: W . n = y by A2, Lm45;

now :: thesis: ex W9 being Walk of G st W9 is_Walk_from x,yend;

hence
ex W9 being Walk of G st W9 is_Walk_from x,y
; :: thesis: verumper cases
( m <= n or n <= m )
;

end;

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

then
W .cut (m,n) is_Walk_from x,y
by A4, A5, A6, Lm16;

hence ex W9 being Walk of G st W9 is_Walk_from x,y ; :: thesis: verum

end;hence ex W9 being Walk of G st W9 is_Walk_from x,y ; :: thesis: verum

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

then
W .cut (n,m) is_Walk_from y,x
by A3, A4, A6, Lm16;

then (W .cut (n,m)) .reverse() is_Walk_from x,y by Th22;

hence ex W9 being Walk of G st W9 is_Walk_from x,y ; :: thesis: verum

end;then (W .cut (n,m)) .reverse() is_Walk_from x,y by Th22;

hence ex W9 being Walk of G st W9 is_Walk_from x,y ; :: thesis: verum