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

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

hence
S is open
; :: thesis: verum
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;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