for S being discrete OrderSortedSign
for M being MSAlgebra over S holds M is order-sorted by ORDERS_3:1;