IntIntervals (a,b) c= bool the carrier of R^1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in IntIntervals (a,b) or x in bool the carrier of R^1 )
assume x in IntIntervals (a,b) ; :: thesis: x in bool the carrier of R^1
then ex n being Element of INT st x = ].(a + n),(b + n).[ ;
hence x in bool the carrier of R^1 by TOPMETR:17; :: thesis: verum
end;
hence IntIntervals (a,b) is Subset-Family of R^1 ; :: thesis: verum