:: deftheorem defines =^ ROUGHS_1:def 15 :
for A being Tolerance_Space
for X, Y being Subset of A holds
( X =^ Y iff UAp X = UAp Y );