:: deftheorem Def7 defines Carr ORDERS_3:def 7 :
for X, b₂ being set holds
( b₂ = Carr X iff for a being set holds
( a in b₂ iff ex s being 1-sorted st
( s in X & a = the carrier of s ) ) );