the carrier' of C c= { (id a) where a is Object of C : verum } by Lm8;
then A1: the carrier' of C c= the carrier' of (IdCat C) by Def20;
the carrier' of (IdCat C) c= the carrier' of C by CAT_2:7;
then the carrier' of (IdCat C) = the carrier' of C by A1;
hence IdCat C = C by Def20, Th6; :: thesis: verum