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

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;