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 A1: X = [.a,1.[ ; :: thesis: X is closed
A2: ( 1 in the carrier of I[01] & 0 in the carrier of I[01] ) by BORSUK_1:86;

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

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

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

end;

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

then X = {} I(01) ;
hence X is closed ; :: thesis: verum

end;

end;