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;

now

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

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;

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

end;

end;

end;

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