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 Th18;
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 3; :: thesis: verum