theorem Th20: :: JORDAN4:20

for f being FinSequence of (TOP-REAL 2)
for i1, i2, i being Nat st 1 <= i1 & i1 < i2 & i2 <= len f & 1 <= i & i < (i2 -' i1) + 1 holds
LSeg ((mid (f,i2,i1)),i) = LSeg (f,(i2 -' i))