let X be non empty set ; :: thesis: for F being Filter of X holds F <> bool X
let F be Filter of X; :: thesis: F <> bool X
assume A1: F = bool X ; :: thesis: contradiction
{} c= X ;
hence contradiction by A1, CARD_FIL:def 1; :: thesis: verum