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

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

( W .find (W . n) <= n & W .rfind (W . n) >= n )

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

( W .find (W . n) <= n & W .rfind (W . n) >= n )

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

assume A1: n <= len W ; :: thesis: ( W .find (W . n) <= n & W .rfind (W . n) >= n )

then A2: W . n in W .vertices() by Lm45;

hence W .find (W . n) <= n by A1, Def19; :: thesis: W .rfind (W . n) >= n

thus W .rfind (W . n) >= n by A1, A2, Def21; :: thesis: verum

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

( W .find (W . n) <= n & W .rfind (W . n) >= n )

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

( W .find (W . n) <= n & W .rfind (W . n) >= n )

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

assume A1: n <= len W ; :: thesis: ( W .find (W . n) <= n & W .rfind (W . n) >= n )

then A2: W . n in W .vertices() by Lm45;

hence W .find (W . n) <= n by A1, Def19; :: thesis: W .rfind (W . n) >= n

thus W .rfind (W . n) >= n by A1, A2, Def21; :: thesis: verum