:: deftheorem defines ERS INTERVA1:def 24 :
for X being Tolerance_Space holds ERS X = [{},{}];