reconsider SFX = {{}} as non empty Subset-Family of X by SETFAM_1:46;
now :: thesis: for x, y being set st x in {{}} & y in {{}} holds
x /\ y in {{}}
let x, y be set ; :: thesis: ( x in {{}} & y in {{}} implies x /\ y in {{}} )
assume ( x in {{}} & y in {{}} ) ; :: thesis: x /\ y in {{}}
then ( x = {} & y = {} ) by TARSKI:def 1;
hence x /\ y in {{}} by TARSKI:def 1; :: thesis: verum
end;
then SFX is cap-closed ;
hence not for b1 being cap-closed Subset-Family of X holds b1 is empty ; :: thesis: verum