:: deftheorem Def21 defines indx PENCIL_1:def 21 :
for I being non empty set
for B being non trivial-yielding Segre-like ManySortedSet of I
for b₃ being Element of I holds
( b₃ = indx B iff not B . b₃ is trivial );