theorem :: FACIRC_2:5

for x being set
for S being non empty strict ManySortedSign
for A being Boolean MSAlgebra over S st x in the carrier of S holds
(SingleMSA x) +* A = MSAlgebra(# the Sorts of A, the Charact of A #)