let G be _Graph; :: thesis: for W being Walk of G holds
( W is directed iff for n being odd Element of NAT st n < len W holds
W . (n + 1) DJoins W . n,W . (n + 2),G )
let W be Walk of G; :: thesis: ( W is directed iff for n being odd Element of NAT st n < len W holds
W . (n + 1) DJoins W . n,W . (n + 2),G )

hereby :: thesis: ( ( for n being odd Element of NAT st n < len W holds
W . (n + 1) DJoins W . n,W . (n + 2),G ) implies W is directed )

assume A1: W is directed ; :: thesis: for n being odd Element of NAT st n < len W holds
W . (n + 1) DJoins W . n,W . (n + 2),G
let n be odd Element of NAT ; :: thesis: ( n < len W implies W . (n + 1) DJoins W . n,W . (n + 2),G )
assume A2: n < len W ; :: thesis: W . (n + 1) DJoins W . n,W . (n + 2),G
then A3: W . (n + 1) Joins W . n,W . (n + 2),G by Def3;
A4: W . n = (the_Source_of G) . (W . (n + 1)) by A1, A2, Def25;

now

assume A5: W . (n + 1) DJoins W . (n + 2),W . n,G ; :: thesis: W . (n + 1) DJoins W . n,W . (n + 2),G
then W . (n + 2) = W . n by A4, GLIB_000:def 16;
hence W . (n + 1) DJoins W . n,W . (n + 2),G by A5; :: thesis: verum

end;

hence W . (n + 1) DJoins W . n,W . (n + 2),G by A3, GLIB_000:19; :: thesis: verum

end;

assume A6: for n being odd Element of NAT st n < len W holds
W . (n + 1) DJoins W . n,W . (n + 2),G ; :: thesis: W is directed

now

let n be odd Element of NAT ; :: thesis: ( n < len W implies (the_Source_of G) . (W . (n + 1)) = W . n )
assume n < len W ; :: thesis: (the_Source_of G) . (W . (n + 1)) = W . n
then W . (n + 1) DJoins W . n,W . (n + 2),G by A6;
hence (the_Source_of G) . (W . (n + 1)) = W . n by GLIB_000:def 16; :: thesis: verum

end;

hence W is directed by Def25; :: thesis: verum