let U be Universe; :: thesis: for C being U -small Category holds C opp is U -small Category
let C be U -small Category; :: thesis: C opp is U -small Category
A1: C is U -element ;
C opp = CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) by OPPCAT_1:def 1;
then C opp is U -element by A1;
hence C opp is U -small Category ; :: thesis: verum