let G be Graph; :: thesis: for e being set st e in the carrier' of G holds
<*e*> is directed Chain of G
let e be set ; :: thesis: ( e in the carrier' of G implies <*e*> is directed Chain of G )
assume A1: e in the carrier' of G ; :: thesis: <*e*> is directed Chain of G
then reconsider s = the Source of G . e, t = the Target of G . e as Element of the carrier of G by FUNCT_2:7;
reconsider E = the carrier' of G as non empty set by A1;
reconsider e = e as Element of E by A1;
<*s,t*> is_vertex_seq_of <*e*> by Th4;
then reconsider c = <*e*> as Chain of G by Def1;
c is directed

proof

let n be Element of NAT ; :: according to GRAPH_1:def 13 :: thesis: ( not 1 <= n or len c <= n or the Source of G . (c . (n + 1)) = the Target of G . (c . n) )
assume ( 1 <= n & n < len c ) ; :: thesis: the Source of G . (c . (n + 1)) = the Target of G . (c . n)
hence the Source of G . (c . (n + 1)) = the Target of G . (c . n) by FINSEQ_1:56; :: thesis: verum

end;

hence <*e*> is directed Chain of G ; :: thesis: verum