set A = the non-empty ManySortedSet of the carrier of S;
ex B being strict non-empty MSAlgebra over S st
( the Sorts of B = the non-empty ManySortedSet of the carrier of S +* ( the bool-sort of S,BOOLEAN) & B is bool-correct ) by Th46;
hence ex b₁ being strict MSAlgebra over S st
( b₁ is bool-correct & b₁ is non-empty ) ; :: thesis: verum