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