for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0)