for r, s being Real st [r,s] in RealOrd holds
r <= s