let a, b be real number ; :: thesis: ( b <= a implies RAT a,b = {} )
assume b <= a ; :: thesis: RAT a,b = {}
then ].a,b.[ = {} by XXREAL_1:28;
hence RAT a,b = {} ; :: thesis: verum