let A be MSAlgebra of S; :: thesis: ( A is Boolean implies ( A is non-empty & A is finite-yielding ) )
assume A1: A is Boolean ; :: thesis: ( A is non-empty & A is finite-yielding )
then the Sorts of A = the carrier of S --> BOOLEAN by Th65;
hence A is non-empty by MSUALG_1:def 3; :: thesis: A is finite-yielding
let v be set ; :: according to FINSET_1:def 4,MSAFREE2:def 11 :: thesis: ( not v in the carrier of S or the Sorts of A . v is finite )
thus ( not v in the carrier of S or the Sorts of A . v is finite ) by A1, Def15; :: thesis: verum