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: ( the carrier of B c= the carrier of A & the Arrows of B cc= the Arrows of A & the Comp of B cc= the Comp of A ) by ALTCAT_2:def 11;
A2: ( A,A opp are_opposite & B,B opp are_opposite ) by YELLOW18:def 4;
then A3: ( the carrier of (A opp ) = the carrier of A & the carrier of (B opp ) = the carrier of B ) by YELLOW18:def 3;
hence the carrier of (B opp ) c= the carrier of (A opp ) by 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 (A opp ) = ~ the Arrows of A & the Arrows of (B opp ) = ~ the Arrows of B ) by A2, YELLOW18:def 3;
hence the Arrows of (B opp ) cc= the Arrows of (A opp ) by A1, Th47; :: thesis: the Comp of (B opp ) cc= the Comp of (A opp )
thus [: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 A1, A3, MCART_1:77; :: according to ALTCAT_2:def 2 :: thesis: for b₁ being set holds
( not b₁ in [:the carrier of (B opp ),the carrier of (B opp ),the carrier of (B opp ):] or the Comp of (B opp ) . b₁ c= the Comp of (A opp ) . 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 set such that
A4: ( x1 in the carrier of B & x2 in the carrier of B & x3 in the carrier of B & x = [x1,x2,x3] ) by A3, MCART_1:72;
reconsider a = x1, b = x2, c = x3 as object of B by A4;
reconsider a1 = a, b1 = b, c1 = c as object of A by A1, A4;
reconsider a' = a, b' = b, c' = c as object of (B opp ) by A2, YELLOW18:def 3;
reconsider a1' = a1, b1' = b1, c1' = c1 as object of (A opp ) by A2, YELLOW18:def 3;
A5: the Comp of (B opp ) . a',b',c' = ~ (the Comp of B . c,b,a) by A2, YELLOW18:def 3;
A6: the Comp of (A opp ) . a1',b1',c1' = ~ (the Comp of A . c1,b1,a1) by A2, YELLOW18:def 3;
A7: [x3,x2,x1] in [:the carrier of B,the carrier of B,the carrier of B:] by A4, MCART_1:73;
A8: ( the Comp of (B opp ) . a',b',c' = the Comp of (B opp ) . x & the Comp of (A opp ) . a1',b1',c1' = the Comp of (A opp ) . x ) by A4, MULTOP_1:def 1;
( the Comp of B . c,b,a = the Comp of B . [c,b,a] & the Comp of A . c1,b1,a1 = the Comp of A . [c1,b1,a1] ) by MULTOP_1:def 1;
then the Comp of B . c,b,a c= the Comp of A . c1,b1,a1 by A1, A7, ALTCAT_2:def 2;
hence the Comp of (B opp ) . x c= the Comp of (A opp ) . x by A5, A6, A8, Th45; :: thesis: verum