:: deftheorem defines is_acyclicpath_of GRAPH_5:def 7 :
for G being Graph
for p being oriented Chain of G
for v1, v2 being Element of G
for V being set holds
( p is_acyclicpath_of v1,v2,V iff ( p is Simple & p is_orientedpath_of v1,v2,V ) );