:: deftheorem defines in2 CAT_4:def 24 :
for C being non empty non void CoprodCatStr
for a, b being Object of C holds in2 (a,b) = the Incl2 of C . (a,b);