:: deftheorem defines = PBOOLE:def 10 :
for I being set
for X, Y being ManySortedSet of I holds
( X = Y iff for i being object st i in I holds
X . i = Y . i );