for R being non empty Poset
for A being OrderSortedSet of R holds id A is order-sorted