theorem :: WAYBEL20:31

for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric lower-bounded RelStr ) holds
for i being Element of I holds (Bottom (product J)) . i = Bottom (J . i)