:: deftheorem defines SingleMSA FACIRC_2:def 2 :
for x being set
for b₂ being strict Boolean MSAlgebra over SingleMSS x holds
( b₂ = SingleMSA x iff verum );