let A be non empty closed_interval Subset of REAL; :: thesis: the carrier of (ClstoCmp A) = A
consider a, b being Real such that
A1: ( a <= b & [.a,b.] = A & ClstoCmp A = Closed-Interval-TSpace (a,b) ) by Def7ClstoCmp;
thus the carrier of (ClstoCmp A) = A by A1, TOPMETR:10; :: thesis: verum