let S be non empty non void ManySortedSign ; :: thesis: 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
let A be non-empty MSAlgebra over 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 ) } ;
A1: { 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 ) }

proof

let x1 be object ; :: 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
A2: ( x1 = x & x is MSCongruence of A ) and
A3: "\/" (X,(EqRelLatt the Sorts of A)) [= x ;

now :: thesis: for q being Element of (EqRelLatt the Sorts of A) st q in X holds
q [= x

let q be Element of (EqRelLatt the Sorts of A); :: thesis: ( q in X implies q [= x )
A4: X is_less_than "\/" (X,(EqRelLatt the Sorts of A)) by LATTICE3:def 21;
assume q in X ; :: thesis: q [= x
then q [= "\/" (X,(EqRelLatt the Sorts of A)) by A4, LATTICE3:def 17;
hence q [= x by A3, LATTICES:7; :: 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 A2; :: thesis: verum

end;

{ 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 object ; :: 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
A5: ( x1 = x & x is MSCongruence of A ) and
A6: X is_less_than x ;
"\/" (X,(EqRelLatt the Sorts of A)) [= x by A6, 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 A5; :: thesis: verum

end;

hence CongrCl ("\/" (X,(EqRelLatt the Sorts of A))) = CongrCl X by A1, XBOOLE_0:def 10; :: thesis: verum