theorem :: TOPMETR:17

the carrier of R^1 = REAL ;