for I being set
for X, Y, Z being ManySortedSet of I st X [= Y & Y [= Z holds
X [= Z ;