thus 1Cat (o,m) is quasi-discrete by ZFMISC_1:def 10; :: according to NATTRA_1:def 20 :: thesis: 1Cat (o,m) is pseudo-discrete
let a be Object of (1Cat (o,m)); :: according to NATTRA_1:def 19 :: thesis: Hom (a,a) is trivial
thus Hom (a,a) is trivial ; :: thesis: verum