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