let G be Graph; :: thesis: for q, p being oriented Chain of G st q in AcyclicPaths p holds
len q <= len p
let q, p be oriented Chain of G; :: thesis: ( q in AcyclicPaths p implies len q <= len p )
assume q in AcyclicPaths p ; :: thesis: len q <= len p
then consider x being oriented Simple Chain of G such that
A1: ( q = x & x <> {} & the Source of G . (x . 1) = the Source of G . (p . 1) & the Target of G . (x . (len x)) = the Target of G . (p . (len p)) & rng x c= rng p ) ;
x is one-to-one by Th20;
then A2: card (rng x) = len x by FINSEQ_4:77;
A3: card (rng x) <= card (rng p) by A1, NAT_1:44;
A4: card (rng p) <= card (dom p) by CARD_2:66;
card (dom p) = card (Seg (len p)) by FINSEQ_1:def 3
.= len p by FINSEQ_1:78 ;
hence len q <= len p by A1, A2, A3, A4, XXREAL_0:2; :: thesis: verum