:: deftheorem Def13 defines RoughSet INTERVA1:def 13 :
for X being Tolerance_Space
for b₂ being Element of [:(bool the carrier of X),(bool the carrier of X):] holds
( b₂ is RoughSet of X iff verum );