for a, b being Real
for B being Subset of I[01] st 0 <= a & a <= b & b <= 1 & B = [.a,b.] holds
Closed-Interval-TSpace (a,b) = I[01] | B by TOPMETR:20, TOPMETR:23;