theorem Th1: :: OSALG_4:1

for R being non empty Poset
for A, B being ManySortedSet of the carrier of R
for OR being ManySortedRelation of A,B st OR is os-compatible holds
OR is OrderSortedSet of R