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