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:46; :: thesis: verum

end;

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