:: deftheorem Def6 defines CongrLatt MSUALG_5:def 6 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for b₃ being strict SubLattice of EqRelLatt the Sorts of A holds
( b₃ = CongrLatt A iff for x being set holds
( x in the carrier of b₃ iff x is MSCongruence of A ) );