A1: ET is U_FMT_filter ;
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 ET ;
take S ; :: thesis: S is open
for x being Element of ET st x in S holds
S in U_FMT x

proof

let x be Element of ET; :: thesis: ( x in S implies S in U_FMT x )
assume x in S ; :: thesis: S in U_FMT x
U_FMT x is Filter of the carrier of ET by A1;
hence S in U_FMT x by CARD_FIL:5; :: thesis: verum

end;

hence S is open ; :: thesis: verum