let U be Universe; :: thesis: for C being U -small Category holds C is U -locally_small
let C be U -small Category; :: thesis: C is U -locally_small

now :: thesis: for x, y being Object of C holds Hom (x,y) is U -set

let x, y be Object of C; :: thesis: Hom (x,y) is U -set
( Hom (x,y) c= the carrier' of C & the carrier' of C is Element of U ) by Def17;
hence Hom (x,y) is U -set by CLASSES4:13; :: thesis: verum

end;

hence C is U -locally_small ; :: thesis: verum