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