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