theorem Th17: :: INTEGRA3:18

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