( {r} is trivial & the carrier of (Closed-Interval-TSpace r,r) = [.r,r.] ) by TOPMETR:25;
hence Closed-Interval-TSpace r,r is trivial by XXREAL_1:17; :: thesis: verum