:: deftheorem defines FMT_R^1 FINTOPO8:def 19 :
FMT_R^1 = Top2NTop R^1;