let C be strict Category; :: thesis: ( C is discrete implies IdCat C = C )
assume A1: C is discrete ; :: thesis: IdCat C = C
the carrier' of C c= { (id a) where a is Object of C : verum }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of C or x in { (id a) where a is Object of C : verum } )
assume x in the carrier' of C ; :: thesis: x in { (id a) where a is Object of C : verum }
then ex a being Object of C st x = id a by A1, Def19;
hence x in { (id a) where a is Object of C : verum } ; :: thesis: verum

end;

then A2: 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:13;
then A3: the carrier' of (IdCat C) = the carrier' of C by A2, XBOOLE_0:def 10;
the carrier of (IdCat C) = the carrier of C by Def20;
hence IdCat C = C by A3, Th10; :: thesis: verum