theorem Th52: :: FINTOPO8:52

the carrier of FMT_R^1 = REAL by TOPMETR:17, FINTOPO7:def 15;