set Z = { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than 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 & X is_less_than 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 & X is_less_than 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 & X is_less_than 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 & X is_less_than 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 & X is_less_than 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 & X is_less_than x ) } ,(EqRelLatt the Sorts of A)) is MSCongruence of A ; :: thesis: verum