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 X9 = X as Subset of I[01] by Th16;
X9 is open by A1, Th42;
hence X is open by TSEP_1:17; :: thesis: verum