:: deftheorem Def4 defines {| ALTCAT_1:def 4 :
for I being set
for G, H being ManySortedSet of [:I,I:]
for b₄ being ManySortedSet of [:I,I,I:] holds
( b₄ = {|G,H|} iff for i, j, k being object st i in I & j in I & k in I holds
b₄ . (i,j,k) = [:(H . (j,k)),(G . (i,j)):] );