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