:: deftheorem Def2 defines RAT_with_denominator MESFUNC1:def 2 :
for n being Nat
for b₂ being Subset of RAT holds
( b₂ = RAT_with_denominator n iff for q being Rational holds
( q in b₂ iff ex i being Integer st q = i / n ) );