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

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

W .rfind n >= n

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

W .rfind n >= n

let n be odd Element of NAT ; :: thesis: ( n <= len W implies W .rfind n >= n )

assume A1: n <= len W ; :: thesis: W .rfind n >= n

then for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= W .rfind n by Def22;

hence W .rfind n >= n by A1; :: thesis: verum

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

W .rfind n >= n

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

W .rfind n >= n

let n be odd Element of NAT ; :: thesis: ( n <= len W implies W .rfind n >= n )

assume A1: n <= len W ; :: thesis: W .rfind n >= n

then for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= W .rfind n by Def22;

hence W .rfind n >= n by A1; :: thesis: verum