:: deftheorem defines @ MSUALG_2:def 12 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for e being Element of SubSort U0 holds @ e = e;