:: deftheorem Def4 defines ManySortedSet INDEX_1:def 4 :
for A, B being set
for b₃ being object holds
( b₃ is ManySortedSet of A,B iff ex f being ManySortedSet of A ex g being ManySortedSet of B st b₃ = [f,g] );