:: deftheorem Def1 defines RAT RAT_1:def 1 :
for b₁ being set holds
( b₁ = RAT iff for x being object holds
( x in b₁ iff ex m, n being Integer st x = m / n ) );