theorem :: WAYBEL29:12

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 & J . i is lower-bounded ) ) holds

for x, y being Element of (product J) holds

( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st

for i being Element of I st not i in K holds

x . i = Bottom (J . i) ) )

for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds

( J . i is up-complete & J . i is lower-bounded ) ) holds

for x, y being Element of (product J) holds

( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st

for i being Element of I st not i in K holds

x . i = Bottom (J . i) ) )