let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for C being Element of (EqRelLatt the Sorts of A) st C is MSCongruence of A holds
CongrCl C = C
let A be non-empty MSAlgebra over S; :: thesis: for C being Element of (EqRelLatt the Sorts of A) st C is MSCongruence of A holds
CongrCl C = C
let C be Element of (EqRelLatt the Sorts of A); :: thesis: ( C is MSCongruence of A implies CongrCl C = C )
set Z = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & C [= x ) } ;

now :: thesis: for q being Element of (EqRelLatt the Sorts of A) st q in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & C [= x ) } holds
C [= q

let q be Element of (EqRelLatt the Sorts of A); :: thesis: ( q in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & C [= x ) } implies C [= q )
assume q in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & C [= x ) } ; :: thesis: C [= q
then ex x being Element of (EqRelLatt the Sorts of A) st
( q = x & x is MSCongruence of A & C [= x ) ;
hence C [= q ; :: thesis: verum

end;

then A1: C is_less_than { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & C [= x ) } by LATTICE3:def 16;
assume C is MSCongruence of A ; :: thesis: CongrCl C = C
then C in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & C [= x ) } ;
hence CongrCl C = C by A1, LATTICE3:41; :: thesis: verum