:: deftheorem defines comma COMMACAT:def 8 :
for C being Category
for c being Object of C holds C comma c = (id C) comma (incl (1Cat c));