for V being set
for G being Graph
for pe being FinSequence of the carrier' of G
for v1, v2, v3 being Element of G
for p, q being oriented Chain of G st q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 holds
q is_orientedpath_of v1,v3,V \/ {v2}