let a, b be real number ; :: thesis: for A being Subset of I[01] st A = [.a,b.] holds
A is closed
let A be Subset of I[01] ; :: thesis: ( A = [.a,b.] implies A is closed )
assume A1: A = [.a,b.] ; :: thesis: A is closed

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

suppose A2: a <= b ; :: thesis: A is closed

then A3: b <= 1 by A1, Th32;
0 <= a by A1, A2, Th32;
then A4: Closed-Interval-TSpace a,b is closed SubSpace of Closed-Interval-TSpace 0 ,1 by A2, A3, TREAL_1:6;
then reconsider BA = the carrier of (Closed-Interval-TSpace a,b) as Subset of (Closed-Interval-TSpace 0 ,1) by BORSUK_1:35;
BA is closed by A4, BORSUK_1:def 14;
hence A is closed by A1, A2, TOPMETR:25, TOPMETR:27; :: thesis: verum

end;

suppose a > b ; :: thesis: A is closed

then A = {} I[01] by A1, XXREAL_1:29;
hence A is closed ; :: thesis: verum

end;

end;