:: deftheorem Def2 defines trivial-yielding MSAFREE4:def 2 :
for I being set
for X being ManySortedSet of I holds
( X is trivial-yielding iff for x being set st x in I holds
X . x is trivial );