let U be Universe; :: thesis: for C being U -locally_small Category st the carrier of C is U -set holds
C is U -small
let C be U -locally_small Category; :: thesis: ( the carrier of C is U -set implies C is U -small )
assume A1: the carrier of C is U -set ; :: thesis: C is U -small
then ( union { (Hom (a,b)) where a, b is Object of C : verum } is Element of U & the carrier' of C c= union { (Hom (a,b)) where a, b is Object of C : verum } ) by CAT_1:92, Th98;
hence C is U -small by A1, CLASSES4:13; :: thesis: verum