let X be Subset of ; :: thesis: for a being Point of st X = ].0 ,a.] holds
X is closed
let a be Point of ; :: 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:86;
then ([#] I(01) ) \ X is open by A3, Th71;
hence X is closed by PRE_TOPC:def 6; :: 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;