the carrier of R^1 = the carrier of TopStruct(# the carrier of RealSpace ,(Family_open_set RealSpace ) #) by PCOMPS_1:def 6;
hence the carrier of R^1 = REAL by METRIC_1:def 14; :: thesis: verum