consider o, m being set ;
take 1Cat o,m ; :: thesis: 1Cat o,m is discrete
let f be Morphism of (1Cat o,m); :: according to NATTRA_1:def 19 :: thesis: ex a being Object of (1Cat o,m) st f = id a
consider a being Object of (1Cat o,m);
take a ; :: thesis: f = id a
thus f = m by TARSKI:def 1
.= id a by TARSKI:def 1 ; :: thesis: verum