:: deftheorem Def2 defines { PZFMISC1:def 2 :
for I being set
for A, B, b₄ being ManySortedSet of I holds
( b₄ = {A,B} iff for i being object st i in I holds
b₄ . i = {(A . i),(B . i)} );