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