theorem Th64: :: FINTOPO8:64

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