let a, b be real number ; :: thesis: ( a >= b implies IRRAT a,b = {} )
assume A1: a >= b ; :: thesis: IRRAT a,b = {}
IRRAT a,b = IRRAT /\ ].a,b.[ by BORSUK_5:def 5
.= IRRAT /\ {} by A1, XXREAL_1:28 ;
hence IRRAT a,b = {} ; :: thesis: verum