let a, b be Real; :: 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, Th13;
0 <= a by A1, A2, Th13;
then A4: Closed-Interval-TSpace (a,b) is closed SubSpace of Closed-Interval-TSpace (0,1) by A2, A3, TREAL_1:3;
then reconsider BA = the carrier of (Closed-Interval-TSpace (a,b)) as Subset of (Closed-Interval-TSpace (0,1)) by BORSUK_1:1;
BA is closed by A4, BORSUK_1:def 11;
hence A is closed by A1, A2, TOPMETR:18, TOPMETR:20; :: 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;