theorem :: SPRECT_3:18

for i, j being Nat
for h being FinSequence of (TOP-REAL 2) st i in dom h & j in dom h holds
L~ (mid (h,i,j)) c= L~ h