IntIntervals a,b c= bool the carrier of R^1

proof

let x be set ; :: 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:24; :: thesis: verum

end;

hence IntIntervals a,b is Subset-Family of R^1 ; :: thesis: verum