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 ( m <= n & n <= len W ) ; :: thesis: ( W .cut m,n is trivial iff m = n )
then A1: (len (W .cut m,n)) + m = n + 1 by Lm15;

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

assume W .cut m,n is trivial ; :: thesis: m = n
then 1 = (n - m) + 1 by A1, Lm55;
hence m = n ; :: thesis: verum

end;

assume m = n ; :: thesis: W .cut m,n is trivial
hence W .cut m,n is trivial by A1, Lm55; :: thesis: verum