:: deftheorem defines DEDEKIND_CUTS ARYTM_2:def 1 :
DEDEKIND_CUTS = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } \ {RAT+};