theorem Th19: :: OSALG_1:19

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