:: deftheorem defines is_orientedpath_of GRAPH_5:def 4 :
for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G
for V being set holds
( p is_orientedpath_of v1,v2,V iff ( p is_orientedpath_of v1,v2 & (vertices p) \ {v2} c= V ) );