:: deftheorem defines RealOrd JORDAN1H:def 1 :
RealOrd = { [r,s] where r, s is Real : r <= s } ;