take
bool X
; :: thesis: ( bool X is compl-closed & bool X is sigma-multiplicative & not bool X is empty )

thus ( bool X is compl-closed & bool X is sigma-multiplicative & not bool X is empty ) ; :: thesis: verum

thus ( bool X is compl-closed & bool X is sigma-multiplicative & not bool X is empty ) ; :: thesis: verum