for S1 being OrderSortedSign
for U1 being monotone OSAlgebra of S1
for U2 being OSSubAlgebra of U1 holds U2 is monotone