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 )

W . (n + 1) DJoins W . n,W . (n + 2),G ; :: thesis: W is directed

( 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 A6:
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;

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

end;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 )

W . (n + 1) Joins W . n,W . (n + 2),G
by A2, Def3;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;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

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

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

hence
W is directed
; :: thesis: verum(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;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