let G be _Graph; :: thesis: for W being Walk of G
for m being odd Element of NAT st m <= len W holds
len (W .cut 1,m) = m
let W be Walk of G; :: thesis: for m being odd Element of NAT st m <= len W holds
len (W .cut 1,m) = m
let m be odd Element of NAT ; :: thesis: ( m <= len W implies len (W .cut 1,m) = m )
assume A1: m <= len W ; :: thesis: len (W .cut 1,m) = m
( not 1 is even & 1 <= m ) by HEYTING3:1, JORDAN12:3;
then (len (W .cut 1,m)) + 1 = m + 1 by A1, Lm15;
hence len (W .cut 1,m) = m ; :: thesis: verum