for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl ("\/" (X,(EqRelLatt the Sorts of A))) = CongrCl X