:: deftheorem defines RoughSet ROUGHS_1:def 8 :
for A being Approximation_Space
for X being Subset of A
for b₃ being set holds
( b₃ is RoughSet of X iff b₃ = [(LAp X),(UAp X)] );