IntIntervals (a,b) is open

proof

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