for h being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat st 1 <= i1 & i1 <= len h & 1 <= i2 & i2 <= len h holds
L~ (mid (h,i1,i2)) c= L~ h