:: deftheorem defines @ INTERVA1:def 22 :
for X being Tolerance_Space
for R being RoughSet of X holds R @ = R;