theorem Th7: :: GRAPHSP:7

for G being Graph
for p being oriented Chain of G
for V being set
for v1, v2 being Vertex of G holds
( p is_orientedpath_of v1,v2,V iff p is_orientedpath_of v1,v2,V \/ {v2} )