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

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

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

end;

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