take Bool M ; :: thesis: ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain )
thus ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain ) ; :: thesis: verum