theorem Th41: :: GRAPH_5:43

for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds
( AcyclicPaths p <> {} & AcyclicPaths (v1,v2) <> {} )