for p being increasing FinSequence of REAL
for i, j being Element of NAT st j in dom p & i <= j holds
mid (p,i,j) is increasing FinSequence of REAL