let G be _Graph; :: thesis: for W being Walk of G
for m, n being Element of NAT
for x, y being set st W is_Walk_from x,y holds
W .remove m,n is_Walk_from x,y
let W be Walk of G; :: thesis: for m, n being Element of NAT
for x, y being set st W is_Walk_from x,y holds
W .remove m,n is_Walk_from x,y
let m, n be Element of NAT ; :: thesis: for x, y being set st W is_Walk_from x,y holds
W .remove m,n is_Walk_from x,y
let x, y be set ; :: thesis: ( W is_Walk_from x,y implies W .remove m,n is_Walk_from x,y )
set W2 = W .remove m,n;
set WA = W .cut 1,m;
set WB = W .cut n,(len W);
assume A1: W is_Walk_from x,y ; :: thesis: W .remove m,n is_Walk_from x,y

now

per cases ( ( not m is even & not n is even & m <= n & n <= len W & W . m = W . n ) or m is even or n is even or not m <= n or not n <= len W or not W . m = W . n ) ;

suppose A2: ( not m is even & not n is even & m <= n & n <= len W & W . m = W . n ) ; :: thesis: W .remove m,n is_Walk_from x,y

then A3: (W .cut n,(len W)) .last() = W .last() by Lm16
.= y by A1, Def23 ;
A4: W .remove m,n = (W .cut 1,m) .append (W .cut n,(len W)) by A2, Def12;
A5: m <= len W by A2, XXREAL_0:2;
A6: 1 <= m by A2, ABIAN:12;
then A7: (W .cut 1,m) .first() = W .first() by A2, A5, Lm16, JORDAN12:3
.= x by A1, Def23 ;
(W .cut 1,m) .last() = W . n by A2, A6, A5, Lm16, JORDAN12:3
.= (W .cut n,(len W)) .first() by A2, Lm16 ;
hence W .remove m,n is_Walk_from x,y by A4, A7, A3, Lm11; :: thesis: verum

end;

suppose ( m is even or n is even or not m <= n or not n <= len W or not W . m = W . n ) ; :: thesis: W .remove m,n is_Walk_from x,y

hence W .remove m,n is_Walk_from x,y by A1, Def12; :: thesis: verum

end;

end;

end;

hence W .remove m,n is_Walk_from x,y ; :: thesis: verum