let X be non empty set ; :: thesis: for SFX being non empty with_non-empty_elements cap-closed upper Subset-Family of X holds SFX is Filter of X
let SFX be non empty with_non-empty_elements cap-closed upper Subset-Family of X; :: thesis: SFX is Filter of X
now :: thesis: ( not {} in SFX & ( for Y1, Y2 being Subset of X st Y1 in SFX & Y2 in SFX holds
Y1 /\ Y2 in SFX ) & ( for Y1, Y2 being Subset of X st Y1 in SFX & Y1 c= Y2 holds
Y2 in SFX ) )
thus not {} in SFX ; :: thesis: ( ( for Y1, Y2 being Subset of X st Y1 in SFX & Y2 in SFX holds
Y1 /\ Y2 in SFX ) & ( for Y1, Y2 being Subset of X st Y1 in SFX & Y1 c= Y2 holds
Y2 in SFX ) )
SFX is cap-closed ;
hence for Y1, Y2 being Subset of X st Y1 in SFX & Y2 in SFX holds
Y1 /\ Y2 in SFX ; :: thesis: for Y1, Y2 being Subset of X st Y1 in SFX & Y1 c= Y2 holds
Y2 in SFX
thus for Y1, Y2 being Subset of X st Y1 in SFX & Y1 c= Y2 holds
Y2 in SFX by def1; :: thesis: verum
end;
hence SFX is Filter of X by CARD_FIL:def 1; :: thesis: verum