let C be strict Category; :: thesis: (C opp) opp = C
C opp is Category ;
then reconsider Copp = CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) as strict Category by OPPCAT_1:def 1;
C opp = Copp by OPPCAT_1:def 1;
then A1: (C opp) opp = CatStr(# the carrier of Copp, the carrier' of Copp, the Target of Copp, the Source of Copp,(~ the Comp of Copp) #) by OPPCAT_1:def 1;
proj1 the Comp of C c= proj1 [:[: the carrier' of C, the carrier' of C:], the carrier' of C:] by XTUPLE_0:8;
hence (C opp) opp = C by A1, FUNCT_4:52; :: thesis: verum