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