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 )
A1: 0 <= a by BORSUK_1:43;
1 in the carrier of I[01] by BORSUK_1:43;
then reconsider B = [.b,1.] as Subset of I[01] by BORSUK_1:40, XXREAL_2:def 12;
0 in the carrier of I[01] by BORSUK_1:43;
then reconsider A = [.0,a.] as Subset of I[01] by BORSUK_1:40, XXREAL_2:def 12;
A2: b <= 1 by BORSUK_1:43;
A3: B is closed by Th20;
A4: A is closed by Th20;
assume X = ].a,b.[ ; :: thesis: X is open
then X = (A \/ B) ` by A1, A2, BORSUK_1:40, XXREAL_1:200;
hence X is open by A4, A3; :: thesis: verum