let U be Universe; :: thesis: for o being object holds not 1Cat (o,U) is U -locally_small
let o9 be object ; :: thesis: not 1Cat (o9,U) is U -locally_small
set C = 1Cat (o9,U);
1Cat (o9,U) = CatStr(# {o9},{U},(U :-> o9),(U :-> o9),((U,U) :-> U) #) by CAT_1:def 11;
then reconsider a = o9 as Object of (1Cat (o9,U)) by TARSKI:def 1;
the carrier' of (1Cat (o9,U)) c= Hom (a,a) by CAT_1:11;
then A1: Hom (a,a) = the carrier' of (1Cat (o9,U)) ;
not 1Cat (o9,U) is U -locally_small

proof

assume 1Cat (o9,U) is U -locally_small ; :: thesis: contradiction
then Hom (a,a) is U -set ;
then {U} is Element of U by A1, COMMACAT:3;
then U in U by Th18;
hence contradiction ; :: thesis: verum

end;

hence not 1Cat (o9,U) is U -locally_small ; :: thesis: verum