theorem Th17: :: OSALG_1:17

for S being OrderSortedSign
for M being MSAlgebra over S holds
( M is order-sorted iff the Sorts of M is OrderSortedSet of S ) by Def16;