for I being set
for y, X being ManySortedSet of I holds
( X = {y} iff for x being ManySortedSet of I holds
( x in X iff x = y ) )