theorem :: CLASSES5:108

for U, V being Universe st U in V holds
Ens U is b₂ -small Category