:: deftheorem Def9 defines denominator ARYTM_3:def 9 :
for x being Element of RAT+
for b₂ being Element of omega holds
( ( x in omega implies ( b₂ = denominator x iff b₂ = 1 ) ) & ( not x in omega implies ( b₂ = denominator x iff ex a being natural Ordinal st x = [a,b₂] ) ) );