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:5;
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 Th3;
then reconsider c = <*e*> as Chain of G by Def1;
c is directed by FINSEQ_1:39;
hence <*e*> is directed Chain of G ; :: thesis: verum