:: deftheorem defines Carrier PRALG_1:def 15 :
for J being set
for A being 1-sorted-yielding ManySortedSet of J
for b₃ being ManySortedSet of J holds
( b₃ = Carrier A iff for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & b₃ . j = the carrier of R ) );