:: deftheorem defines OrientedPaths GRAPH_5:def 5 :
for G being Graph
for v1, v2 being Element of G holds OrientedPaths (v1,v2) = { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } ;