:: deftheorem defines TRS INTERVA1:def 25 :
for X being Tolerance_Space holds TRS X = [([#] X),([#] X)];