let ET be non empty strict FMT_Space_Str ; :: thesis: ( ET is U_FMT_filter_base implies gen_filter ET is U_FMT_filter )
assume A1: ET is U_FMT_filter_base ; :: thesis: gen_filter ET is U_FMT_filter
for x being Element of (gen_filter ET) holds U_FMT x is Filter of the carrier of (gen_filter ET)

proof

let x be Element of (gen_filter ET); :: thesis: U_FMT x is Filter of the carrier of (gen_filter ET)
reconsider x0 = x as Element of ET ;
U_FMT x0 is filter_base of the carrier of ET by A1;
then <.(U_FMT x0).] is Filter of the carrier of ET by CARDFIL2:25;
hence U_FMT x is Filter of the carrier of (gen_filter ET) by Def7; :: thesis: verum

end;

hence gen_filter ET is U_FMT_filter ; :: thesis: verum