theorem Th11: :: WAYBEL29:11

for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds J . i is up-complete ) holds
I -POS_prod J is up-complete