:: deftheorem defines R^1 TOPMETR:def 6 :
R^1 = TopSpaceMetr RealSpace;