theorem :: EQUATION:16
for I being set
for A being ManySortedSet of I holds (id A) "" A = A