for r, s being Real
for f being increasing FinSequence of REAL st rng f = {r,s} & len f = 2 & r <= s holds
( f . 1 = r & f . 2 = s )