let a, b be Real; for A being Subset of I[01] st A = [.a,b.] holds
A is closed
let A be Subset of I[01]; ( A = [.a,b.] implies A is closed )
assume A1:
A = [.a,b.]
; A is closed
per cases
( a <= b or a > b )
;
suppose A2:
a <= b
;
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;
verum end; end;