let C be Subcategory of A; :: thesis: C is discrete
A1: the carrier of C c= the carrier of A by CAT_2:def 4;
thus C is quasi-discrete :: according to NATTRA_1:def 20 :: thesis: C is pseudo-discrete
proof
let a, b be Element of C; :: according to NATTRA_1:def 18 :: thesis: ( Hom (a,b) <> {} implies a = b )
reconsider aa = a, bb = b as Element of A by A1;
assume A2: Hom (a,b) <> {} ; :: thesis: a = b
Hom (a,b) c= Hom (aa,bb) by CAT_2:def 4;
then Hom (aa,bb) <> {} by A2;
hence a = b by Def17; :: thesis: verum
end;
let a be Element of C; :: according to NATTRA_1:def 19 :: thesis: Hom (a,a) is trivial
reconsider aa = a as Element of A by A1;
Hom (a,a) c= Hom (aa,aa) by CAT_2:def 4;
hence Hom (a,a) is trivial ; :: thesis: verum