let G be _Graph; :: thesis: for W being Walk of G
for m, n being Element of NAT st W is directed holds
W .cut m,n is directed
let W be Walk of G; :: thesis: for m, n being Element of NAT st W is directed holds
W .cut m,n is directed
let m, n be Element of NAT ; :: thesis: ( W is directed implies W .cut m,n is directed )
set W2 = W .cut m,n;
assume A1: W is directed ; :: thesis: W .cut m,n is directed

now

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

suppose A2: ( not m is even & not n is even & m <= n & n <= len W ) ; :: thesis: W .cut m,n is directed

then reconsider m9 = m as odd Element of NAT ;

now

let x be odd Element of NAT ; :: thesis: ( x < len (W .cut m,n) implies (W .cut m,n) . (x + 1) DJoins (W .cut m,n) . x,(W .cut m,n) . (x + 2),G )
reconsider xaa1 = x - 1 as even Element of NAT by HEYTING3:1, INT_1:18;
assume A3: x < len (W .cut m,n) ; :: thesis: (W .cut m,n) . (x + 1) DJoins (W .cut m,n) . x,(W .cut m,n) . (x + 2),G
then x + 1 <= len (W .cut m,n) by NAT_1:13;
then A4: x + 1 < len (W .cut m,n) by XXREAL_0:1;
m + x in dom W by A2, A3, Lm15;
then m9 + x <= len W by FINSEQ_3:27;
then A5: (m9 + x) - 1 < (len W) - 0 by XREAL_1:17;
xaa1 < (len (W .cut m,n)) - 0 by A3, XREAL_1:16;
then A6: (W .cut m,n) . (xaa1 + 1) = W . (m + xaa1) by A2, Lm15;
A7: (W .cut m,n) . (x + 2) = (W .cut m,n) . ((x + 1) + 1)
.= W . (m + (((x - 1) + 1) + 1)) by A2, A4, Lm15
.= W . ((m + xaa1) + 2) ;
(W .cut m,n) . (x + 1) = W . (((m + x) - 1) + 1) by A2, A3, Lm15
.= W . ((m + xaa1) + 1) ;
hence (W .cut m,n) . (x + 1) DJoins (W .cut m,n) . x,(W .cut m,n) . (x + 2),G by A1, A6, A5, A7, Lm51; :: thesis: verum

end;

hence W .cut m,n is directed by Lm51; :: thesis: verum

end;

suppose ( m is even or n is even or not m <= n or not n <= len W ) ; :: thesis: W .cut m,n is directed

hence W .cut m,n is directed by A1, Def11; :: thesis: verum

end;

end;

end;

hence W .cut m,n is directed ; :: thesis: verum