let C be non empty transitive AltCatStr ; :: thesis: ex C' being non empty transitive strict AltCatStr st C,C' are_opposite
deffunc H₁( set , set ) -> set = the Arrows of C . $2,$1;
deffunc H₂( set , set , set , set , set ) -> set = (the Comp of C . $3,$2,$1) . $4,$5;

A1: now

let a, b, c be Element of C; :: thesis: for f, g being set st f in H₁(a,b) & g in H₁(b,c) holds
H₂(a,b,c,f,g) in H₁(a,c)
let f, g be set ; :: thesis: ( f in H₁(a,b) & g in H₁(b,c) implies H₂(a,b,c,f,g) in H₁(a,c) )
reconsider a' = a, b' = b, c' = c as object of C ;
assume A2: f in H₁(a,b) ; :: thesis: ( g in H₁(b,c) implies H₂(a,b,c,f,g) in H₁(a,c) )
then A3: f in <^b',a'^> ;
reconsider f' = f as Morphism of b',a' by A2;
assume A4: g in H₁(b,c) ; :: thesis: H₂(a,b,c,f,g) in H₁(a,c)
then A5: g in <^c',b'^> ;
reconsider g' = g as Morphism of c',b' by A4;
A6: ( <^c',a'^> <> {} & H₁(a,c) = <^c',a'^> ) by A3, A5, ALTCAT_1:def 4;
H₂(a,b,c,f,g) = f' * g' by A2, A4, ALTCAT_1:def 10;
hence H₂(a,b,c,f,g) in H₁(a,c) by A6; :: thesis: verum

end;

ex C1 being non empty transitive strict AltCatStr st
( the carrier of C1 = the carrier of C & ( for a, b being object of C1 holds <^a,b^> = H₁(a,b) ) & ( for a, b, c being object of C1 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = H₂(a,b,c,f,g) ) ) from YELLOW18:sch 1(A1);
then consider C1 being non empty transitive strict AltCatStr such that
A7: the carrier of C1 = the carrier of C and
A8: for a, b being object of C1 holds <^a,b^> = the Arrows of C . b,a and
A9: for a, b, c being object of C1 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (the Comp of C . c,b,a) . f,g ;
take C1 ; :: thesis: C,C1 are_opposite

now

let a, b, c be object of C; :: thesis: for a', b', c' being object of C1 st a' = a & b' = b & c' = c holds
( <^a,b^> = <^b',a'^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = f & g' = g holds
f' * g' = g * f ) )
let a', b', c' be object of C1; :: thesis: ( a' = a & b' = b & c' = c implies ( <^a,b^> = <^b',a'^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = f & g' = g holds
f' * g' = g * f ) ) )
assume A10: ( a' = a & b' = b & c' = c ) ; :: thesis: ( <^a,b^> = <^b',a'^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = f & g' = g holds
f' * g' = g * f ) )
hence A11: <^a,b^> = <^b',a'^> by A8; :: thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = f & g' = g holds
f' * g' = g * f )
A12: <^b,c^> = <^c',b'^> by A8, A10;
assume A13: ( <^a,b^> <> {} & <^b,c^> <> {} ) ; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = f & g' = g holds
f' * g' = g * f
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c
for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = f & g' = g holds
f' * g' = g * f
let g be Morphism of b,c; :: thesis: for f' being Morphism of b',a'
for g' being Morphism of c',b' st f' = f & g' = g holds
f' * g' = g * f
let f' be Morphism of b',a'; :: thesis: for g' being Morphism of c',b' st f' = f & g' = g holds
f' * g' = g * f
let g' be Morphism of c',b'; :: thesis: ( f' = f & g' = g implies f' * g' = g * f )
assume ( f' = f & g' = g ) ; :: thesis: f' * g' = g * f
hence f' * g' = (the Comp of C . a,b,c) . g,f by A9, A10, A11, A12, A13
.= g * f by A13, ALTCAT_1:def 10 ;
:: thesis: verum

end;

hence C,C1 are_opposite by A7, Th9; :: thesis: verum