for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I
for X being Subset of (product J) st ex_sup_of X, product J holds
for i being Element of I holds (sup X) . i = sup (pi (X,i))