for G being Graph
for p, q being oriented Chain of G st q in AcyclicPaths p holds
len q <= len p