let a, b be real number ; :: thesis: for X being Subset of st X = ].a,b.[ holds
Int X = ].a,b.[
let X be Subset of ; :: 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 by BORSUK_5:62;
Int X = X by TOPS_1:55;
hence Int X = ].a,b.[ by A1; :: thesis: verum