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 lower-bounded algebraic LATTICE ) holds
product J is lower-bounded algebraic LATTICE