let G be _Graph; 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; ( 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 ( ( 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
;
for n being odd Element of NAT st n < len W holds
W . (n + 1) DJoins W . n,W . (n + 2),Glet n be
odd Element of
NAT ;
( n < len W implies W . (n + 1) DJoins W . n,W . (n + 2),G )assume A2:
n < len W
;
W . (n + 1) DJoins W . n,W . (n + 2),Gthen A3:
W . n = (the_Source_of G) . (W . (n + 1))
by A1;
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;
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
; W is directed
hence
W is directed
; verum