:: deftheorem defines QuotMSAlg MSUALG_4:def 14 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1 holds QuotMSAlg (U1,R) = MSAlgebra(# (Class R),(QuotCharact R) #);