:: deftheorem defines IRRAT BORSUK_5:def 1 :
IRRAT = REAL \ RAT;