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