let G be Graph; :: thesis: for p being oriented Chain of G holds AcyclicPaths p c= AcyclicPaths G
let p be oriented Chain of G; :: thesis: AcyclicPaths p c= AcyclicPaths G
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in AcyclicPaths p or e in AcyclicPaths G )
assume e in AcyclicPaths p ; :: thesis: e in AcyclicPaths G
then ex q being oriented Simple Chain of G st
( e = q & q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) ;
hence e in AcyclicPaths G ; :: thesis: verum