for I being non empty set
for A being 1-sorted-yielding non-Empty ManySortedSet of I
for B being Element of Carrier A holds {B} is ManySortedSubset of Carrier A