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

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

let x, y be Object of (C opp); :: thesis: Hom (x,y) is U -set
reconsider oy = opp y, ox = opp x as Object of C ;
Hom (x,y) = Hom (oy,ox) by OPPCAT_1:6;
hence Hom (x,y) is U -set by Def36; :: thesis: verum

end;

hence C opp is U -locally_small Category by Def36; :: thesis: verum