:: deftheorem defines EmptyMS CAT_4:def 21 :
for C being non empty non void CoprodCatStr holds EmptyMS C = the Initial of C;