let a, b be Real; :: 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 3
.= IRRAT /\ {} by A1, XXREAL_1:28 ;
hence IRRAT (a,b) = {} ; :: thesis: verum