let C be Chain of G; :: thesis: ( C is empty implies C is oriented )
assume A1: C is empty ; :: thesis: C is oriented
let n be Element of NAT ; :: according to GRAPH_1:def 13 :: thesis: ( 1 <= n & n < len C implies the Source of G . (C . (n + 1)) = the Target of G . (C . n) )
thus ( 1 <= n & n < len C implies the Source of G . (C . (n + 1)) = the Target of G . (C . n) ) by A1, CARD_1:27, XXREAL_0:2; :: thesis: verum