:: deftheorem Def3 defines denominator RAT_1:def 3 :
for p being Rational
for b₂ being Nat holds
( b₂ = denominator p iff ( b₂ <> 0 & ex m being Integer st p = m / b₂ & ( for n being Integer
for k being Nat st k <> 0 & p = n / k holds
b₂ <= k ) ) );