let C be Category; :: thesis: ( C is quasi-discrete implies the carrier' of C = union { (Hom (a,a)) where a is Element of C : verum } )
assume A1: C is quasi-discrete ; :: thesis: the carrier' of C = union { (Hom (a,a)) where a is Element of C : verum }
set A = { (Hom (a,b)) where a, b is Element of C : verum } ;
set N = union { (Hom (a,b)) where a, b is Element of C : verum } ;
set B = { (Hom (a,a)) where a is Element of C : verum } ;
set M = union { (Hom (a,a)) where a is Element of C : verum } ;
A2: the carrier' of C = union { (Hom (a,b)) where a, b is Element of C : verum } by CAT_1:92;
thus the carrier' of C c= union { (Hom (a,a)) where a is Element of C : verum } :: according to XBOOLE_0:def 10 :: thesis: union { (Hom (a,a)) where a is Element of C : verum } c= the carrier' of C

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the carrier' of C or e in union { (Hom (a,a)) where a is Element of C : verum } )
assume e in the carrier' of C ; :: thesis: e in union { (Hom (a,a)) where a is Element of C : verum }
then consider X being set such that
A3: e in X and
A4: X in { (Hom (a,b)) where a, b is Element of C : verum } by A2, TARSKI:def 4;
consider a, b being Element of C such that
A5: X = Hom (a,b) by A4;
a = b by A1, A3, A5;
then X in { (Hom (a,a)) where a is Element of C : verum } by A5;
hence e in union { (Hom (a,a)) where a is Element of C : verum } by A3, TARSKI:def 4; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union { (Hom (a,a)) where a is Element of C : verum } or e in the carrier' of C )
assume e in union { (Hom (a,a)) where a is Element of C : verum } ; :: thesis: e in the carrier' of C
then consider X being set such that
A6: e in X and
A7: X in { (Hom (a,a)) where a is Element of C : verum } by TARSKI:def 4;
ex a being Element of C st X = Hom (a,a) by A7;
hence e in the carrier' of C by A6; :: thesis: verum