IntIntervals (a,b) is open

proof

let A be Subset of R^1; :: according to TOPS_2:def 1 :: thesis: ( not A in IntIntervals (a,b) or A is open )
assume A in IntIntervals (a,b) ; :: thesis: A is open
then ex n being Element of INT st A = ].(a + n),(b + n).[ ;
hence A is open by JORDAN6:35; :: thesis: verum

end;

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