:: deftheorem Def20 defines RoughSets INTERVA1:def 20 :
for X being Tolerance_Space
for b₂ being set holds
( b₂ = RoughSets X iff for x being set holds
( x in b₂ iff x is RoughSet of X ) );