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 :: thesis: W .cut (m,n) is directed

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

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

then reconsider m9 = m as odd Element of NAT ;

now :: thesis: for x being odd Element of NAT st x < len (W .cut (m,n)) holds
(W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G

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 ABIAN:12, INT_1:5;
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:25;
then A5: (m9 + x) - 1 < (len W) - 0 by XREAL_1:15;
xaa1 < (len (W .cut (m,n))) - 0 by A3, XREAL_1:14;
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 ( not m is odd or not n is odd 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