let X be non empty set ; :: thesis: for S being set holds

( S in Filters X iff S is Filter of X )

let S be set ; :: thesis: ( S in Filters X iff S is Filter of X )

thus ( S in Filters X implies S is Filter of X ) :: thesis: ( S is Filter of X implies S in Filters X )

hence S in Filters X ; :: thesis: verum

( S in Filters X iff S is Filter of X )

let S be set ; :: thesis: ( S in Filters X iff S is Filter of X )

thus ( S in Filters X implies S is Filter of X ) :: thesis: ( S is Filter of X implies S in Filters X )

proof

assume
S is Filter of X
; :: thesis: S in Filters X
defpred S_{1}[ set ] means $1 is Filter of X;

assume S in Filters X ; :: thesis: S is Filter of X

then A1: S in { S1 where S1 is Subset-Family of X : S_{1}[S1] }
;

thus S_{1}[S]
from CARD_FIL:sch 1(A1); :: thesis: verum

end;assume S in Filters X ; :: thesis: S is Filter of X

then A1: S in { S1 where S1 is Subset-Family of X : S

thus S

hence S in Filters X ; :: thesis: verum