:: deftheorem defines MSCharact MSUALG_1:def 10 :
for A being Universal_Algebra holds MSCharact A = the charact of A;