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