let C be Category; ( C is discrete implies the carrier' of C c= { (id a) where a is Element of C : verum } )
assume A1:
C is discrete
; the carrier' of C c= { (id a) where a is Element of C : verum }
let e be object ; TARSKI:def 3 ( not e in the carrier' of C or e in { (id a) where a is Element of C : verum } )
assume
e in the carrier' of C
; e in { (id a) where a is Element of C : verum }
then
e in union { (Hom (a,a)) where a is Element of C : verum }
by A1, Lm6;
then consider X being set such that
A2:
e in X
and
A3:
X in { (Hom (a,a)) where a is Element of C : verum }
by TARSKI:def 4;
consider a being Element of C such that
A4:
X = Hom (a,a)
by A3;
X = {(id a)}
by A4, A1, Lm7;
then
e = id a
by A2, TARSKI:def 1;
hence
e in { (id b) where b is Element of C : verum }
; verum