let X be Subset of I(01) ; :: thesis: for a, b being Point of I[01] st X = ].a,b.[ holds
X is open
let a, b be Point of I[01] ; :: thesis: ( X = ].a,b.[ implies X is open )
assume A1: X = ].a,b.[ ; :: thesis: X is open
then reconsider X' = X as Subset of I[01] by Th44;
X' is open by A1, Th70;
hence X is open by Th59, TSEP_1:17; :: thesis: verum