theorem Th8: :: CAT_8:8

for x being object
for C being CategoryStr st the carrier of C = {x} & the composition of C = {[[x,x],x]} holds
C is non empty category