:: deftheorem defines REAL+ ARYTM_2:def 2 :
REAL+ = (RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ;