for I being non empty set
for A being ManySortedSet of I
for i being Element of I
for S being non trivial set holds not A +* (i,S) is trivial-yielding