:: deftheorem defines MSSorts MSUALG_1:def 9 :
for A being Universal_Algebra holds MSSorts A = 0 .--> the carrier of A;