:: deftheorem defines IRRAT BORSUK_5:def 3 :
for a, b being Real holds IRRAT (a,b) = IRRAT /\ ].a,b.[;