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