:: deftheorem Def17 defines order-sorted OSALG_1:def 17 :
for S being OrderSortedSign
for M being MSAlgebra over S holds
( M is order-sorted iff for s1, s2 being SortSymbol of S st s1 <= s2 holds
the Sorts of M . s1 c= the Sorts of M . s2 );