for S1 being OrderSortedSign
for U0 being strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice U0) = U0