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