theorem Th9: :: LFUZZY_0:9

for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is sup-Semilattice ) holds
product J is with_suprema