let X be Subset of I(01); :: thesis: for a being Point of I[01] st X = ].0,a.] holds
X is closed
let a be Point of I[01]; :: thesis: ( X = ].0,a.] implies X is closed )
assume A1: X = ].0,a.] ; :: thesis: X is closed

per cases ( 0 < a or 0 >= a ) ;

suppose A2: 0 < a ; :: thesis: X is closed

[#] I(01) = ].0,1.[ by Def1;
then A3: ([#] I(01)) \ X = ].a,1.[ by A1, A2, XXREAL_1:187;
1 in the carrier of I[01] by BORSUK_1:43;
then ([#] I(01)) \ X is open by A3, Th43;
hence X is closed by PRE_TOPC:def 3; :: thesis: verum

end;

suppose 0 >= a ; :: thesis: X is closed

then X = {} I(01) by A1, XXREAL_1:26;
hence X is closed ; :: thesis: verum

end;

end;