:: deftheorem defines @ INTERVA1:def 21 :
for X being Tolerance_Space
for R being Element of RoughSets X holds @ R = R;