theorem :: TOPREALB:3

for a, b being Real
for x being set holds
( x in IntIntervals (a,b) iff ex n being Element of INT st x = ].(a + n),(b + n).[ ) ;