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

<*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