set Z = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ;

now :: thesis: for z being object st z in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } holds
z in the carrier of (CongrLatt A)

let z be object ; :: thesis: ( z in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } implies z in the carrier of (CongrLatt A) )
assume z in { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ; :: thesis: z in the carrier of (CongrLatt A)
then ex z1 being Element of (EqRelLatt the Sorts of A) st
( z = z1 & z1 is MSCongruence of A & E [= z1 ) ;
hence z in the carrier of (CongrLatt A) by MSUALG_5:def 6; :: thesis: verum

end;

then reconsider Z9 = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } as Subset of (CongrLatt A) by TARSKI:def 3;
"/\" (Z9,(EqRelLatt the Sorts of A)) is MSCongruence of A by Th11;
hence "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A)) is MSCongruence of A ; :: thesis: verum