:: deftheorem defines RS INTERVA1:def 14 :
for X being Tolerance_Space
for A being Subset of X holds RS A = [(LAp A),(UAp A)];