theorem Th7: :: OSALG_3:7

for R being non empty Poset
for A being OrderSortedSet of R
for F being ManySortedFunction of the carrier of R st F is order-sorted holds
F .:.: A is OrderSortedSet of R