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