:: deftheorem defines QuotUnivAlg ALG_1:def 10 :
for U1 being Universal_Algebra
for E being Congruence of U1 holds QuotUnivAlg (U1,E) = UAStr(# (Class E),(QuotOpSeq (U1,E)) #);