( {r} is 1 -element & the carrier of (Closed-Interval-TSpace (r,r)) = [.r,r.] ) by TOPMETR:18;
hence the carrier of (Closed-Interval-TSpace (r,r)) is 1 -element by XXREAL_1:17; :: according to STRUCT_0:def 19 :: thesis: verum