:: deftheorem Def3 defines DEDEKIND_CUT ARYTM_2:def 3 :
for x being Element of REAL+
for b₂ being Element of DEDEKIND_CUTS holds
( ( x in RAT+ implies ( b₂ = DEDEKIND_CUT x iff ex r being Element of RAT+ st
( x = r & b₂ = { s where s is Element of RAT+ : s < r } ) ) ) & ( not x in RAT+ implies ( b₂ = DEDEKIND_CUT x iff b₂ = x ) ) );