theorem Th16: :: JORDAN3:16

for f, g being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for j being Nat st p in L~ f & g = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) & 1 <= j & j + 1 <= len g holds
LSeg (g,j) c= LSeg (f,(((Index (p,f)) + j) -' 1))