let G be Graph; :: thesis: for e being set st e in the carrier' of G holds
<*e*> is oriented Simple Chain of G
let e be set ; :: thesis: ( e in the carrier' of G implies <*e*> is oriented Simple Chain of G )
assume e in the carrier' of G ; :: thesis: <*e*> is oriented Simple Chain of G
then A1: <*e*> is FinSequence of the carrier' of G by FINSEQ_1:74;
len <*e*> = 1 by FINSEQ_1:40;
hence <*e*> is oriented Simple Chain of G by A1, GRAPH_5:15; :: thesis: verum