theorem Th16: :: OSALG_1:16

for R being non empty Poset
for z being non empty set holds ConstOSSet (R,z) is order-sorted by Th15;