let a, b be Real; :: thesis: for X being Subset of R^1 st X = ].a,b.[ holds
Int X = ].a,b.[
let X be Subset of R^1; :: thesis: ( X = ].a,b.[ implies Int X = ].a,b.[ )
assume A1: X = ].a,b.[ ; :: thesis: Int X = ].a,b.[
then reconsider X = X as open Subset of R^1 by BORSUK_5:39;
Int X = X by TOPS_1:23;
hence Int X = ].a,b.[ by A1; :: thesis: verum