theorem Th11: :: CAT_5:11

for C being Category holds 1Cat (C,[[C,C],(id C)]) is Categorial