theorem :: OSALG_1:28

for S being OrderSortedSign
for A being OSAlgebra of S st ( S is discrete or S is op-discrete ) holds
A is monotone