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