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