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