:: deftheorem defines oriented GRAPH_1:def 15 :
for G being Graph
for IT being Chain of G holds
( IT is oriented iff for n being Nat st 1 <= n & n < len IT holds
the Source of G . (IT . (n + 1)) = the Target of G . (IT . n) );