let S be non empty non void ManySortedSign ; :: thesis: for U0 being strict non-empty MSAlgebra of S holds Top (MSSubAlLattice U0) = U0
let U0 be strict non-empty MSAlgebra of S; :: thesis: Top (MSSubAlLattice U0) = U0
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
thus Top (MSSubAlLattice U0) = GenMSAlg B by Th36
.= U0 by Th22 ; :: thesis: verum