let S1 be OrderSortedSign; :: thesis: for U0 being strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice U0) = U0
let U0 be strict non-empty OSAlgebra of S1; :: thesis: Top (OSSubAlLattice U0) = U0
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 23;
B is OrderSortedSet of by OSALG_1:17;
then reconsider B = the Sorts of U0 as OSSubset of U0 by Def2;
thus Top (OSSubAlLattice U0) = GenOSAlg B by Th55
.= U0 by Th39 ; :: thesis: verum