:: deftheorem defines Element PBOOLE:def 14 :
for I being set
for B, b₃ being ManySortedSet of I holds
( b₃ is Element of B iff for i being object st i in I holds
b₃ . i is Element of B . i );