A1: 0 in the carrier of I[01] by BORSUK_1:86;
let X be Subset of I(01) ; :: thesis: for a being Point of I[01] st X = [.a,1.[ holds
X is closed
let a be Point of I[01] ; :: thesis: ( X = [.a,1.[ implies X is closed )
assume A2: X = [.a,1.[ ; :: thesis: X is closed

per cases ( not X is empty or X is empty ) ;

suppose A3: not X is empty ; :: thesis: X is closed

A4: a <= 1 by BORSUK_1:86;
a <> 1 by A2, A3, XXREAL_1:18;
then A5: a < 1 by A4, XXREAL_0:1;
[#] I(01) = ].0 ,1.[ by Def1;
then ([#] I(01) ) \ X = ].0 ,a.[ by A2, A5, XXREAL_1:195;
then ([#] I(01) ) \ X is open by A1, Th71;
hence X is closed by PRE_TOPC:def 6; :: thesis: verum

end;

suppose X is empty ; :: thesis: X is closed

hence X is closed ; :: thesis: verum

end;

end;