reconsider S = bool X as Subset-Family of X by ZFMISC_1:def 1;
take S ; :: thesis: ( not S is empty & S is compl-closed & S is cap-closed )
thus not S is empty ; :: thesis: ( S is compl-closed & S is cap-closed )
thus S is compl-closed :: thesis: S is cap-closed

proof

let A be Subset of X; :: according to PROB_1:def 1 :: thesis: ( A in S implies A ` in S )
thus ( A in S implies A ` in S ) ; :: thesis: verum

end;

thus S is cap-closed :: thesis: verum

proof

let A, B be set ; :: according to FINSUB_1:def 2 :: thesis: ( not A in S or not B in S or A /\ B in S )
assume ( A in S & B in S ) ; :: thesis: A /\ B in S
then A /\ B c= X by XBOOLE_1:108;
hence A /\ B in S ; :: thesis: verum

end;