let A be MSAlgebra over 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 Th57;
hence A is non-empty ; :: thesis: A is finite-yielding
let v be object ; :: according to FINSET_1:def 5,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; :: thesis: verum