theorem Th20: :: CAT_8:20

for C being non empty with_identities CategoryStr
for a being Object of C st a is terminal holds
for h being Morphism of a,a holds id- a = h