let X be Subset of I[01] ; :: thesis: for a being Point of I[01] st X = ].a,1.] holds
X is open
let a be Point of I[01] ; :: thesis: ( X = ].a,1.] implies X is open )
assume A1: X = ].a,1.] ; :: thesis: X is open
set Y = [.0 ,a.];
[.0 ,a.] c= the carrier of I[01]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [.0 ,a.] or x in the carrier of I[01] )
assume A2: x in [.0 ,a.] ; :: thesis: x in the carrier of I[01]
then reconsider x = x as Real ;
A3: 0 <= x by A2, XXREAL_1:1;
A4: x <= a by A2, XXREAL_1:1;
a <= 1 by BORSUK_1:86;
then x <= 1 by A4, XXREAL_0:2;
hence x in the carrier of I[01] by A3, BORSUK_1:86; :: thesis: verum

end;

then reconsider Y = [.0 ,a.] as Subset of I[01] ;
A5: Y is closed by BORSUK_4:48;
X ` = Y by A1, Th2;
hence X is open by A5, TOPS_1:30; :: thesis: verum