let a, b be real number ; :: thesis: ( a <= b implies Closed-Interval-TSpace a,b is closed SubSpace of R^1 )
assume a <= b ; :: thesis: Closed-Interval-TSpace a,b is closed SubSpace of R^1
then the carrier of (Closed-Interval-TSpace a,b) = [.a,b.] by TOPMETR:25;
then for A being Subset of R^1 st A = the carrier of (Closed-Interval-TSpace a,b) holds
A is closed by Th4;
hence Closed-Interval-TSpace a,b is closed SubSpace of R^1 by BORSUK_1:def 14; :: thesis: verum