:: deftheorem defines RAT NUMBERS:def 3 :
RAT = (RAT+ \/ [:{0},RAT+:]) \ {[0,0]};