theorem Th109: :: CLASSES5:107

for U being Universe holds
( Ens U is non b₁ -small Category & the carrier of (Ens U) is U -Class & the carrier' of (Ens U) is U -Class )