:: deftheorem defines is_orientedpath_of GRAPH_5:def 3 :
for G being Graph
for p being oriented Chain of G
for v1, v2 being Element of G holds
( p is_orientedpath_of v1,v2 iff ( p <> {} & the Source of G . (p . 1) = v1 & the Target of G . (p . (len p)) = v2 ) );