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