for R being non empty Poset
for A, B being OrderSortedSet of R
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" & F is order-sorted holds
F "" is order-sorted