theorem :: FINTOPO8:67

gen_filter gen_R^1 = FMT_R^1