:: deftheorem defines [| PBOOLE:def 16 :
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):] );