theorem Th2: :: PENCIL_3:2

for I being non empty set
for i being Element of I
for A being 1-sorted-yielding non-Trivial-yielding ManySortedSet of I holds not A . i is trivial