take Bool M ; :: thesis: ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain & Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )
thus ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain & Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound ) by Lm1; :: thesis: verum