:: deftheorem Def8 defines -carrier_of YELLOW18:def 8 :
for C being category
for a, b₃ being set holds
( ( a is Object of C implies ( b₃ = C -carrier_of a iff ex b being Object of C st
( b = a & b₃ = proj1 (idm b) ) ) ) & ( a is not Object of C implies ( b₃ = C -carrier_of a iff b₃ = {} ) ) );