:: deftheorem defines [1] CAT_4:def 3 :
for C being non empty non void ProdCatStr holds [1] C = the TerminalObj of C;