let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S holds CongrLatt A is /\-inheriting
let A be non-empty MSAlgebra over S; :: thesis: CongrLatt A is /\-inheriting
set E = EqRelLatt the Sorts of A;
set C = CongrLatt A;

now :: thesis: for B being Subset of (CongrLatt A) holds "/\" (B,(EqRelLatt the Sorts of A)) in the carrier of (CongrLatt A)

let B be Subset of (CongrLatt A); :: thesis: "/\" (B,(EqRelLatt the Sorts of A)) in the carrier of (CongrLatt A)
reconsider d = "/\" (B,(EqRelLatt the Sorts of A)) as MSCongruence of A by Th11;
d in the carrier of (CongrLatt A) by MSUALG_5:def 6;
hence "/\" (B,(EqRelLatt the Sorts of A)) in the carrier of (CongrLatt A) ; :: thesis: verum

end;

hence CongrLatt A is /\-inheriting by MSUALG_7:def 2; :: thesis: verum