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

for m, n being odd Element of NAT st m <= n & n <= len W holds

( W .cut (m,n) is trivial iff m = n )

let W be Walk of G; :: thesis: for m, n being odd Element of NAT st m <= n & n <= len W holds

( W .cut (m,n) is trivial iff m = n )

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W implies ( W .cut (m,n) is trivial iff m = n ) )

assume that

A1: m <= n and

A2: n <= len W ; :: thesis: ( W .cut (m,n) is trivial iff m = n )

A3: (len (W .cut (m,n))) + m = n + 1 by A1, A2, Lm15;

hence W .cut (m,n) is trivial by A3, Lm55; :: thesis: verum

for m, n being odd Element of NAT st m <= n & n <= len W holds

( W .cut (m,n) is trivial iff m = n )

let W be Walk of G; :: thesis: for m, n being odd Element of NAT st m <= n & n <= len W holds

( W .cut (m,n) is trivial iff m = n )

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W implies ( W .cut (m,n) is trivial iff m = n ) )

assume that

A1: m <= n and

A2: n <= len W ; :: thesis: ( W .cut (m,n) is trivial iff m = n )

A3: (len (W .cut (m,n))) + m = n + 1 by A1, A2, Lm15;

hereby :: thesis: ( m = n implies W .cut (m,n) is trivial )

assume
m = n
; :: thesis: W .cut (m,n) is trivial assume
W .cut (m,n) is trivial
; :: thesis: m = n

then 1 = (n - m) + 1 by A3, Lm55;

hence m = n ; :: thesis: verum

end;then 1 = (n - m) + 1 by A3, Lm55;

hence m = n ; :: thesis: verum

hence W .cut (m,n) is trivial by A3, Lm55; :: thesis: verum