set C = the U -element Category;
take the U -element Category ; :: thesis: the U -element Category is U -locally_small

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

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

end;

hence the U -element Category is U -locally_small ; :: thesis: verum