theorem :: FINTOPO8:59

for x being object holds
( x is Point of FMT_R^1 iff x is Point of RealSpace ) by METRIC_1:def 13, TOPMETR:17, FINTOPO7:def 15;