theorem Th9: :: OSALG_1:9

for S being OrderSortedSign st S is op-discrete holds
S is monotone