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