:: deftheorem defines AcyclicPaths GRAPH_5:def 10 :
for G being Graph
for p being oriented Chain of G holds AcyclicPaths p = { q where q is oriented Simple Chain of G : ( 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 ) } ;