let S be discrete OrderSortedSign; :: thesis: for M being MSAlgebra of S holds M is order-sorted
let M be MSAlgebra of S; :: thesis: M is order-sorted
let s1, s2 be SortSymbol of S; :: according to OSALG_1:def 17 :: thesis: ( s1 <= s2 implies the Sorts of M . s1 c= the Sorts of M . s2 )
assume s1 <= s2 ; :: thesis: the Sorts of M . s1 c= the Sorts of M . s2
hence the Sorts of M . s1 c= the Sorts of M . s2 by ORDERS_3:1; :: thesis: verum