theorem Th4: :: OSALG_3:4

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