theorem :: WAYBEL20:32

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 upper-bounded RelStr ) holds
for i being Element of I holds (Top (product J)) . i = Top (J . i)