for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S holds Top (CongrLatt A) = [| the Sorts of A, the Sorts of A|]