let A be non empty transitive AltCatStr ; :: thesis: for B being non empty transitive SubCatStr of A holds B opp is SubCatStr of A opp

let B be non empty transitive SubCatStr of A; :: thesis: B opp is SubCatStr of A opp

A1: B,B opp are_opposite by YELLOW18:def 4;

then A2: the carrier of (B opp) = the carrier of B by YELLOW18:def 3;

A3: the Arrows of (B opp) = ~ the Arrows of B by A1, YELLOW18:def 3;

A4: A,A opp are_opposite by YELLOW18:def 4;

then A5: the carrier of (A opp) = the carrier of A by YELLOW18:def 3;

hence the carrier of (B opp) c= the carrier of (A opp) by A2, ALTCAT_2:def 11; :: according to ALTCAT_2:def 11 :: thesis: ( the Arrows of (B opp) cc= the Arrows of (A opp) & the Comp of (B opp) cc= the Comp of (A opp) )

( the Arrows of B cc= the Arrows of A & the Arrows of (A opp) = ~ the Arrows of A ) by A4, ALTCAT_2:def 11, YELLOW18:def 3;

hence the Arrows of (B opp) cc= the Arrows of (A opp) by A3, Th46; :: thesis: the Comp of (B opp) cc= the Comp of (A opp)

A6: the carrier of B c= the carrier of A by ALTCAT_2:def 11;

hence [: the carrier of (B opp), the carrier of (B opp), the carrier of (B opp):] c= [: the carrier of (A opp), the carrier of (A opp), the carrier of (A opp):] by A5, A2, MCART_1:73; :: according to ALTCAT_2:def 2 :: thesis: for b_{1} being set holds

( not b_{1} in [: the carrier of (B opp), the carrier of (B opp), the carrier of (B opp):] or the Comp of (B opp) . b_{1} c= the Comp of (A opp) . b_{1} )

let x be set ; :: thesis: ( not x in [: the carrier of (B opp), the carrier of (B opp), the carrier of (B opp):] or the Comp of (B opp) . x c= the Comp of (A opp) . x )

assume x in [: the carrier of (B opp), the carrier of (B opp), the carrier of (B opp):] ; :: thesis: the Comp of (B opp) . x c= the Comp of (A opp) . x

then consider x1, x2, x3 being object such that

A7: ( x1 in the carrier of B & x2 in the carrier of B & x3 in the carrier of B ) and

A8: x = [x1,x2,x3] by A2, MCART_1:68;

reconsider a = x1, b = x2, c = x3 as Object of B by A7;

reconsider a1 = a, b1 = b, c1 = c as Object of A by A6;

reconsider a19 = a1, b19 = b1, c19 = c1 as Object of (A opp) by A4, YELLOW18:def 3;

A9: ( the Comp of B cc= the Comp of A & the Comp of B . (c,b,a) = the Comp of B . [c,b,a] ) by ALTCAT_2:def 11, MULTOP_1:def 1;

A10: the Comp of A . (c1,b1,a1) = the Comp of A . [c1,b1,a1] by MULTOP_1:def 1;

[x3,x2,x1] in [: the carrier of B, the carrier of B, the carrier of B:] by A7, MCART_1:69;

then A11: the Comp of B . (c,b,a) c= the Comp of A . (c1,b1,a1) by A9, A10;

reconsider a9 = a, b9 = b, c9 = c as Object of (B opp) by A1, YELLOW18:def 3;

A12: ( the Comp of (B opp) . (a9,b9,c9) = the Comp of (B opp) . x & the Comp of (A opp) . (a19,b19,c19) = the Comp of (A opp) . x ) by A8, MULTOP_1:def 1;

A13: the Comp of (A opp) . (a19,b19,c19) = ~ ( the Comp of A . (c1,b1,a1)) by A4, YELLOW18:def 3;

the Comp of (B opp) . (a9,b9,c9) = ~ ( the Comp of B . (c,b,a)) by A1, YELLOW18:def 3;

hence the Comp of (B opp) . x c= the Comp of (A opp) . x by A13, A12, A11, Th44; :: thesis: verum

let B be non empty transitive SubCatStr of A; :: thesis: B opp is SubCatStr of A opp

A1: B,B opp are_opposite by YELLOW18:def 4;

then A2: the carrier of (B opp) = the carrier of B by YELLOW18:def 3;

A3: the Arrows of (B opp) = ~ the Arrows of B by A1, YELLOW18:def 3;

A4: A,A opp are_opposite by YELLOW18:def 4;

then A5: the carrier of (A opp) = the carrier of A by YELLOW18:def 3;

hence the carrier of (B opp) c= the carrier of (A opp) by A2, ALTCAT_2:def 11; :: according to ALTCAT_2:def 11 :: thesis: ( the Arrows of (B opp) cc= the Arrows of (A opp) & the Comp of (B opp) cc= the Comp of (A opp) )

( the Arrows of B cc= the Arrows of A & the Arrows of (A opp) = ~ the Arrows of A ) by A4, ALTCAT_2:def 11, YELLOW18:def 3;

hence the Arrows of (B opp) cc= the Arrows of (A opp) by A3, Th46; :: thesis: the Comp of (B opp) cc= the Comp of (A opp)

A6: the carrier of B c= the carrier of A by ALTCAT_2:def 11;

hence [: the carrier of (B opp), the carrier of (B opp), the carrier of (B opp):] c= [: the carrier of (A opp), the carrier of (A opp), the carrier of (A opp):] by A5, A2, MCART_1:73; :: according to ALTCAT_2:def 2 :: thesis: for b

( not b

let x be set ; :: thesis: ( not x in [: the carrier of (B opp), the carrier of (B opp), the carrier of (B opp):] or the Comp of (B opp) . x c= the Comp of (A opp) . x )

assume x in [: the carrier of (B opp), the carrier of (B opp), the carrier of (B opp):] ; :: thesis: the Comp of (B opp) . x c= the Comp of (A opp) . x

then consider x1, x2, x3 being object such that

A7: ( x1 in the carrier of B & x2 in the carrier of B & x3 in the carrier of B ) and

A8: x = [x1,x2,x3] by A2, MCART_1:68;

reconsider a = x1, b = x2, c = x3 as Object of B by A7;

reconsider a1 = a, b1 = b, c1 = c as Object of A by A6;

reconsider a19 = a1, b19 = b1, c19 = c1 as Object of (A opp) by A4, YELLOW18:def 3;

A9: ( the Comp of B cc= the Comp of A & the Comp of B . (c,b,a) = the Comp of B . [c,b,a] ) by ALTCAT_2:def 11, MULTOP_1:def 1;

A10: the Comp of A . (c1,b1,a1) = the Comp of A . [c1,b1,a1] by MULTOP_1:def 1;

[x3,x2,x1] in [: the carrier of B, the carrier of B, the carrier of B:] by A7, MCART_1:69;

then A11: the Comp of B . (c,b,a) c= the Comp of A . (c1,b1,a1) by A9, A10;

reconsider a9 = a, b9 = b, c9 = c as Object of (B opp) by A1, YELLOW18:def 3;

A12: ( the Comp of (B opp) . (a9,b9,c9) = the Comp of (B opp) . x & the Comp of (A opp) . (a19,b19,c19) = the Comp of (A opp) . x ) by A8, MULTOP_1:def 1;

A13: the Comp of (A opp) . (a19,b19,c19) = ~ ( the Comp of A . (c1,b1,a1)) by A4, YELLOW18:def 3;

the Comp of (B opp) . (a9,b9,c9) = ~ ( the Comp of B . (c,b,a)) by A1, YELLOW18:def 3;

hence the Comp of (B opp) . x c= the Comp of (A opp) . x by A13, A12, A11, Th44; :: thesis: verum