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