let X be non empty set ; :: thesis: for FX being Filter of X holds FX is non empty with_non-empty_elements cap-closed upper Subset-Family of X
let FX be Filter of X; :: thesis: FX is non empty with_non-empty_elements cap-closed upper Subset-Family of X
( not FX is empty & FX is with_non-empty_elements & FX is cap-closed & FX is upper ) by CARD_FIL:def 1;
hence FX is non empty with_non-empty_elements cap-closed upper Subset-Family of X ; :: thesis: verum