:: deftheorem defines gen_filter FINTOPO7:def 10 :
for ET being non empty strict FMT_Space_Str holds gen_filter ET = FMT_Space_Str(# the carrier of ET,<.ET.] #);