:: deftheorem Def16 defines order-sorted OSALG_1:def 16 :
for R being non empty Poset
for M being ManySortedSet of R holds
( M is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds
M . s1 c= M . s2 );