:: deftheorem Def5 defines (/\) PBOOLE:def 5 :
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) );