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 ;
consider n being odd Element of NAT such that
A5: n <= len W and
A6: W . n = y by ;
now :: thesis: ex W9 being Walk of G st W9 is_Walk_from x,y
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
end;
end;
end;
hence ex W9 being Walk of G st W9 is_Walk_from x,y ; :: thesis: verum