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 18;
B is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = the Sorts of U0 as OSSubset of U0 by Def2;
thus Top (OSSubAlLattice U0) = GenOSAlg B by Th50
.= U0 by Th34 ; :: thesis: verum