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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in [.a,1.] or x in the carrier of I[01] )
A2: 0 <= a by BORSUK_1:43;
assume A3: x in [.a,1.] ; :: thesis: x in the carrier of I[01]
then reconsider x = x as Real ;
( x <= 1 & a <= x ) by A3, XXREAL_1:1;
hence x in the carrier of I[01] by A2, BORSUK_1:43; :: thesis: verum

end;

then reconsider Y = [.a,1.] as Subset of I[01] ;
( Y is closed & X ` = Y ) by A1, Th3, BORSUK_4:23;
hence X is open by TOPS_1:4; :: thesis: verum