:: deftheorem Def4 defines product YELLOW_1:def 4 :
for I being set
for J being RelStr-yielding ManySortedSet of I
for b₃ being strict RelStr holds
( b₃ = product J iff ( the carrier of b₃ = product (Carrier J) & ( for x, y being Element of b₃ st x in product (Carrier J) holds
( x <= y iff ex f, g being Function st
( f = x & g = y & ( for i being object st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) ) ) ) );