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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in [.0,a.] or x in the carrier of I[01] )
A2: a <= 1 by BORSUK_1:43;
assume A3: x in [.0,a.] ; :: thesis: x in the carrier of I[01]
then reconsider x = x as Real ;
A4: 0 <= x by A3, XXREAL_1:1;
x <= a by A3, XXREAL_1:1;
then x <= 1 by A2, XXREAL_0:2;
hence x in the carrier of I[01] by A4, BORSUK_1:43; :: thesis: verum
end;
then reconsider Y = [.0,a.] as Subset of I[01] ;
( Y is closed & X ` = Y ) by A1, Th2, BORSUK_4:23;
hence X is open by TOPS_1:4; :: thesis: verum