:: deftheorem Def6 defines [\ INT_1:def 6 :
for r being Real
for b₂ being Integer holds
( b₂ = [\r/] iff ( b₂ <= r & r - 1 < b₂ ) );