for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being MSCongruence of A holds C is ManySortedSubset of [| the Sorts of A, the Sorts of A|]