let G be _Graph; :: thesis: for W being Walk of G

for n, m being Element of NAT holds (W .cut (m,n)) .edges() c= W .edges()

let W be Walk of G; :: thesis: for n, m being Element of NAT holds (W .cut (m,n)) .edges() c= W .edges()

let n, m be Element of NAT ; :: thesis: (W .cut (m,n)) .edges() c= W .edges()

for n, m being Element of NAT holds (W .cut (m,n)) .edges() c= W .edges()

let W be Walk of G; :: thesis: for n, m being Element of NAT holds (W .cut (m,n)) .edges() c= W .edges()

let n, m be Element of NAT ; :: thesis: (W .cut (m,n)) .edges() c= W .edges()

now :: thesis: (W .cut (m,n)) .edges() c= W .edges() end;

hence
(W .cut (m,n)) .edges() c= W .edges()
; :: thesis: verumper 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 )
;

end;

suppose A1:
( m is odd & n is odd & m <= n & n <= len W )
; :: thesis: (W .cut (m,n)) .edges() c= W .edges()

then reconsider m9 = m as odd Element of NAT ;

end;now :: thesis: for e being object st e in (W .cut (m,n)) .edges() holds

e in W .edges()

hence
(W .cut (m,n)) .edges() c= W .edges()
by TARSKI:def 3; :: thesis: verume in W .edges()

let e be object ; :: thesis: ( e in (W .cut (m,n)) .edges() implies e in W .edges() )

assume e in (W .cut (m,n)) .edges() ; :: thesis: e in W .edges()

then consider x being even Element of NAT such that

A2: 1 <= x and

A3: x <= len (W .cut (m,n)) and

A4: (W .cut (m,n)) . x = e by Lm46;

reconsider xaa1 = x - 1 as odd Element of NAT by A2, INT_1:5;

A5: xaa1 < (len (W .cut (m,n))) - 0 by A3, XREAL_1:15;

then A6: m + xaa1 in dom W by A1, Lm15;

then A7: m9 + xaa1 <= len W by FINSEQ_3:25;

xaa1 + 1 = x ;

then A8: e = W . (m + xaa1) by A1, A4, A5, Lm15;

1 <= m9 + xaa1 by A6, FINSEQ_3:25;

hence e in W .edges() by A8, A7, Lm46; :: thesis: verum

end;assume e in (W .cut (m,n)) .edges() ; :: thesis: e in W .edges()

then consider x being even Element of NAT such that

A2: 1 <= x and

A3: x <= len (W .cut (m,n)) and

A4: (W .cut (m,n)) . x = e by Lm46;

reconsider xaa1 = x - 1 as odd Element of NAT by A2, INT_1:5;

A5: xaa1 < (len (W .cut (m,n))) - 0 by A3, XREAL_1:15;

then A6: m + xaa1 in dom W by A1, Lm15;

then A7: m9 + xaa1 <= len W by FINSEQ_3:25;

xaa1 + 1 = x ;

then A8: e = W . (m + xaa1) by A1, A4, A5, Lm15;

1 <= m9 + xaa1 by A6, FINSEQ_3:25;

hence e in W .edges() by A8, A7, Lm46; :: thesis: verum