theorem :: GRAPH_5:30

for x being set
for G being Graph
for v1, v2 being Element of G holds
( x in OrientedPaths (v1,v2) iff ex p being oriented Chain of G st
( p = x & p is_orientedpath_of v1,v2 ) ) ;