for C being Category holds C ~= Alter (alter C) by Th51;