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 ) )
hereby :: thesis: ( ex n being odd Element of NAT st
( 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;
given n being odd Element of NAT such that A4: n < len W and
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