for r being Real
for p being FinSequence of REAL st ( for i being Nat st i in dom p holds
r <= p . i ) & ex i0 being Nat st
( i0 in dom p & p . i0 = r ) holds
r = inf (rng p)