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