:: deftheorem Def12 defines ObCat ALTCAT_2:def 12 :
for C being non empty AltCatStr
for o being Object of C
for b₃ being strict SubCatStr of C holds
( b₃ = ObCat o iff ( the carrier of b₃ = {o} & the Arrows of b₃ = (o,o) :-> <^o,o^> & the Comp of b₃ = [o,o,o] .--> ( the Comp of C . (o,o,o)) ) );