for S being non empty ManySortedSign
for A being MSAlgebra over S holds
( A is Boolean iff rng the Sorts of A c= {BOOLEAN} )