theorem :: CLASSES5:60

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