:: deftheorem defines = INTERVA1:def 17 :
for X being Tolerance_Space
for A, B being RoughSet of X holds
( A = B iff ( LAp A = LAp B & UAp A = UAp B ) );