reconsider F = bool X as non empty Subset-Family of X ;
take F ; :: thesis: ( F is compl-closed & F is sigma-multiplicative & not F is empty )
thus ( ( for A being Subset of X st A in F holds
A ` in F ) & ( for A1 being SetSequence of X st rng A1 c= F holds
Intersection A1 in F ) ) ; :: according to PROB_1:def 1,PROB_1:def 8 :: thesis: not F is empty
thus not F is empty ; :: thesis: verum