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