:: deftheorem defines IntIntervals TOPREALB:def 1 :
for a, b being Real holds IntIntervals (a,b) = { ].(a + n),(b + n).[ where n is Element of INT : verum } ;