theorem :: GRAPH_5:36

for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_acyclicpath_of v1,v2 holds
p is_orientedpath_of v1,v2 ;