theorem :: CLASSES5:100

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