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