theorem Th12: :: OSALG_1:12

for SM being monotone OrderSortedSign st SM is op-discrete holds
SM is regular