:: deftheorem Def6 defines Class MSUALG_4:def 6 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1
for b₄ being V8() ManySortedSet of the carrier of S holds
( b₄ = Class R iff for s being Element of S holds b₄ . s = Class (R . s) );