bool X is compl-closed

proof

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

end;

hence for b₁ being Subset-Family of X st b₁ = bool X holds
b₁ is compl-closed ; :: thesis: verum