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

for e being set holds

( e in W .edges() iff ex n being odd Element of NAT st

( n < len W & W . (n + 1) = e ) )

let W be Walk of G; :: thesis: for e being set holds

( e in W .edges() iff ex n being odd Element of NAT st

( n < len W & W . (n + 1) = e ) )

let e be set ; :: thesis: ( e in W .edges() iff ex n being odd Element of NAT st

( n < len W & W . (n + 1) = e ) )

A5: W . (n + 1) = e ; :: thesis: e in W .edges()

A6: 1 <= n + 1 by NAT_1:12;

n + 1 <= len W by A4, NAT_1:13;

hence e in W .edges() by A5, A6, Lm46; :: thesis: verum

for e being set holds

( e in W .edges() iff ex n being odd Element of NAT st

( n < len W & W . (n + 1) = e ) )

let W be Walk of G; :: thesis: for e being set holds

( e in W .edges() iff ex n being odd Element of NAT st

( n < len W & W . (n + 1) = e ) )

let e be set ; :: thesis: ( e in W .edges() iff ex n being odd Element of NAT st

( n < len W & W . (n + 1) = e ) )

hereby :: thesis: ( ex n being odd Element of NAT st

( n < len W & W . (n + 1) = e ) implies e in W .edges() )

given n being odd Element of NAT such that A4:
n < len W
and ( n < len W & W . (n + 1) = e ) implies e in W .edges() )

assume
e in W .edges()
; :: thesis: ex n being odd Element of NAT st

( n < len W & W . (n + 1) = e )

then consider n1 being even Element of NAT such that

A1: 1 <= n1 and

A2: n1 <= len W and

A3: W . n1 = e by Lm46;

reconsider n = n1 - 1 as odd Element of NAT by A1, INT_1:5;

take n = n; :: thesis: ( n < len W & W . (n + 1) = e )

n1 - 1 < (len W) - 0 by A2, XREAL_1:15;

hence n < len W ; :: thesis: W . (n + 1) = e

thus W . (n + 1) = e by A3; :: thesis: verum

end;( n < len W & W . (n + 1) = e )

then consider n1 being even Element of NAT such that

A1: 1 <= n1 and

A2: n1 <= len W and

A3: W . n1 = e by Lm46;

reconsider n = n1 - 1 as odd Element of NAT by A1, INT_1:5;

take n = n; :: thesis: ( n < len W & W . (n + 1) = e )

n1 - 1 < (len W) - 0 by A2, XREAL_1:15;

hence n < len W ; :: thesis: W . (n + 1) = e

thus W . (n + 1) = e by A3; :: thesis: verum

A5: W . (n + 1) = e ; :: thesis: e in W .edges()

A6: 1 <= n + 1 by NAT_1:12;

n + 1 <= len W by A4, NAT_1:13;

hence e in W .edges() by A5, A6, Lm46; :: thesis: verum