let U, V be Universe; :: thesis: ( U in V implies Ens U is V -small Category )
assume A1: U in V ; :: thesis: Ens U is V -small Category
( the carrier of (Ens U) is U -Class & the carrier' of (Ens U) is U -Class ) by Th109;
then Ens U is V -element by A1, CLASSES4:13;
hence Ens U is V -small Category ; :: thesis: verum