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 b₁ being cap-closed Subset-Family of X holds b₁ is empty ; :: thesis: verum