:: deftheorem defines AcyclicPaths GRAPH_5:def 8 :
for G being Graph
for v1, v2 being Element of G holds AcyclicPaths (v1,v2) = { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } ;