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

proof

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

end;

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