theorem Th64: :: CLASSES5:62

for U being Universe ex C being b₁ -petit Category st
( the carrier of C is Element of U & the carrier' of C is not Element of U )