for A being category
for a being Object of A
for x being set holds
( x in (Concretized A) -carrier_of a iff ex b being Object of A ex f being Morphism of b,a st
( <^b,a^> <> {} & x = [f,[b,a]] ) )