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 & 1 <= j & j + 1 <= len g & g = (mid (f,1,(Index (p,f)))) ^ <*p*> holds
LSeg (g,j) c= LSeg (f,j)