A1: 0 in the carrier of I[01] by BORSUK_1:43;
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:43;
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, Th43;
hence X is closed by PRE_TOPC:def 3; :: thesis: verum
end;
suppose X is empty ; :: thesis: X is closed
hence X is closed ; :: thesis: verum
end;
end;