:: deftheorem Def1 defines OrderSortedSubset OSALG_2:def 1 :
for R being non empty Poset
for M being OrderSortedSet of R
for b₃ being ManySortedSubset of M holds
( b₃ is OrderSortedSubset of M iff b₃ is OrderSortedSet of R );