:: deftheorem defines UAp INTERVA1:def 16 :
for X being Tolerance_Space
for A being RoughSet of X holds UAp A = A `2 ;