:: deftheorem defines QuotOSAlg OSALG_4:def 20 :
for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 holds QuotOSAlg (U1,R) = MSAlgebra(# (OSClass R),(OSQuotCharact R) #);