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