theorem :: CAT_6:52
for C being non empty category holds C ~= alter (Alter C)