let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl ("\/" X,(EqRelLatt the Sorts of A)) = CongrCl X
let A be non-empty MSAlgebra of S; :: thesis: for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl ("\/" X,(EqRelLatt the Sorts of A)) = CongrCl X
let X be Subset of (EqRelLatt the Sorts of A); :: thesis: CongrCl ("\/" X,(EqRelLatt the Sorts of A)) = CongrCl X
set D1 = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" X,(EqRelLatt the Sorts of A) [= x ) } ;
set D2 = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ;
{ x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" X,(EqRelLatt the Sorts of A) [= x ) } = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) }

proof

thus { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" X,(EqRelLatt the Sorts of A) [= x ) } c= { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } :: according to XBOOLE_0:def 10 :: thesis: { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } c= { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" X,(EqRelLatt the Sorts of A) [= x ) }

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" X,(EqRelLatt the Sorts of A) [= x ) } or x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } )
assume x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" X,(EqRelLatt the Sorts of A) [= x ) } ; :: thesis: x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) }
then consider x being Element of (EqRelLatt the Sorts of A) such that
A1: ( x1 = x & x is MSCongruence of A & "\/" X,(EqRelLatt the Sorts of A) [= x ) ;

now

let q be Element of (EqRelLatt the Sorts of A); :: thesis: ( q in X implies q [= x )
assume A2: q in X ; :: thesis: q [= x
X is_less_than "\/" X,(EqRelLatt the Sorts of A) by LATTICE3:def 21;
then q [= "\/" X,(EqRelLatt the Sorts of A) by A2, LATTICE3:def 17;
hence q [= x by A1, LATTICES:25; :: thesis: verum

end;

then X is_less_than x by LATTICE3:def 17;
hence x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } by A1; :: thesis: verum

end;

thus { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } c= { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" X,(EqRelLatt the Sorts of A) [= x ) } :: thesis: verum

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } or x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" X,(EqRelLatt the Sorts of A) [= x ) } )
assume x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ; :: thesis: x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" X,(EqRelLatt the Sorts of A) [= x ) }
then consider x being Element of (EqRelLatt the Sorts of A) such that
A3: ( x1 = x & x is MSCongruence of A & X is_less_than x ) ;
"\/" X,(EqRelLatt the Sorts of A) [= x by A3, LATTICE3:def 21;
hence x1 in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & "\/" X,(EqRelLatt the Sorts of A) [= x ) } by A3; :: thesis: verum

end;

end;

hence CongrCl ("\/" X,(EqRelLatt the Sorts of A)) = CongrCl X ; :: thesis: verum