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

proof

hence
IntIntervals (a,b) is Subset-Family of R^1
; :: thesis: verum
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;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