:: deftheorem defines MSAlg MSUALG_1:def 11 :
for A being Universal_Algebra holds MSAlg A = MSAlgebra(# (MSSorts A),(MSCharact A) #);