theorem :: SPRECT_3:19

for i, j being Nat st 1 <= i & i < j holds
for f being FinSequence of (TOP-REAL 2) st j <= len f holds
L~ (mid (f,i,j)) = (LSeg (f,i)) \/ (L~ (mid (f,(i + 1),j)))