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