:: deftheorem defines gen_R^1 FINTOPO8:def 21 :
gen_R^1 = FMT_Space_Str(# the carrier of FMT_R^1,gen_NS_R^1 #);