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 W' being Walk of G st W' 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 W' being Walk of G st W' is_Walk_from x,y
let x, y be set ; :: thesis: ( x in W .vertices() & y in W .vertices() implies ex W' being Walk of G st W' is_Walk_from x,y )
assume that
A1: x in W .vertices() and
A2: y in W .vertices() ; :: thesis: ex W' being Walk of G st W' 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 W' being Walk of G st W' is_Walk_from x,y

then W .cut m,n is_Walk_from x,y by A4, A5, A6, Lm16;
hence ex W' being Walk of G st W' is_Walk_from x,y ; :: thesis: verum

end;

suppose n <= m ; :: thesis: ex W' being Walk of G st W' 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 W' being Walk of G st W' is_Walk_from x,y ; :: thesis: verum

end;

end;

end;

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