set S = the carrier of ET;

the carrier of ET c= the carrier of ET ;

then reconsider S = the carrier of ET as Subset of the carrier of ET ;

take S ; :: thesis: for x being Element of ET st x in A holds

S in U_FMT x

the carrier of ET c= the carrier of ET ;

then reconsider S = the carrier of ET as Subset of the carrier of ET ;

take S ; :: thesis: for x being Element of ET st x in A holds

S in U_FMT x

hereby :: thesis: verum

let x be Element of ET; :: thesis: ( x in A implies S in U_FMT x )

assume x in A ; :: thesis: S in U_FMT x

U_FMT x is Filter of the carrier of ET by Def2;

hence S in U_FMT x by CARD_FIL:5; :: thesis: verum

end;assume x in A ; :: thesis: S in U_FMT x

U_FMT x is Filter of the carrier of ET by Def2;

hence S in U_FMT x by CARD_FIL:5; :: thesis: verum