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)

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

hence
gen_filter ET is U_FMT_filter
; :: thesis: verum
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;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