:: deftheorem Def26 defines Cocartesian CAT_4:def 26 :
for IT being non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr holds
( IT is Cocartesian iff ( the Initial of IT is initial & ( for a, b being Object of IT holds
( dom ( the Incl1 of IT . (a,b)) = a & dom ( the Incl2 of IT . (a,b)) = b & the Coproduct of IT . (a,b) is_a_coproduct_wrt the Incl1 of IT . (a,b), the Incl2 of IT . (a,b) ) ) ) );