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