( {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