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