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 = (the_Source_of G) . (W . (n + 1)) by A1;
A4: now :: thesis: ( W . (n + 1) DJoins W . (n + 2),W . n,G implies W . (n + 1) DJoins W . n,W . (n + 2),G )
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 A3, GLIB_000:def 14;
hence W . (n + 1) DJoins W . n,W . (n + 2),G by A5; :: thesis: verum
end;
W . (n + 1) Joins W . n,W . (n + 2),G by A2, Def3;
hence W . (n + 1) DJoins W . n,W . (n + 2),G by A4, GLIB_000:16; :: 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 :: thesis: for n being odd Element of NAT st n < len W holds
(the_Source_of G) . (W . (n + 1)) = W . n
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 14; :: thesis: verum
end;
hence W is directed ; :: thesis: verum