theorem :: CLASSES5:99

for U being Universe
for C being b₁ -small Category holds C opp is b₁ -small Category