theorem :: FINTOPO8:2

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