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 ; :: 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 ;
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 , 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 , by A4;
A6: <^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 holds <^a,b^> = H₁(a,b) ) & ( for a, b, c being object of st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of ,
for g being Morphism of , 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 holds <^a,b^> = the Arrows of C . b,a and
A9: for a, b, c being object of st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of ,
for g being Morphism of , 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 ; :: thesis: for a', b', c' being object of st a' = a & b' = b & c' = c holds
( <^a,b^> = <^b',a'^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of ,
for g being Morphism of ,
for f' being Morphism of ,
for g' being Morphism of , st f' = f & g' = g holds
f' * g' = g * f ) )
let a', b', c' be object of ; :: thesis: ( a' = a & b' = b & c' = c implies ( <^a,b^> = <^b',a'^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of ,
for g being Morphism of ,
for f' being Morphism of ,
for g' being Morphism of , st f' = f & g' = g holds
f' * g' = g * f ) ) )
assume that
A10: a' = a and
A11: b' = b and
A12: c' = c ; :: thesis: ( <^a,b^> = <^b',a'^> & ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of ,
for g being Morphism of ,
for f' being Morphism of ,
for g' being Morphism of , st f' = f & g' = g holds
f' * g' = g * f ) )
thus A13: <^a,b^> = <^b',a'^> by A8, A10, A11; :: thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of ,
for g being Morphism of ,
for f' being Morphism of ,
for g' being Morphism of , st f' = f & g' = g holds
f' * g' = g * f )
A14: <^b,c^> = <^c',b'^> by A8, A11, A12;
assume that
A15: <^a,b^> <> {} and
A16: <^b,c^> <> {} ; :: thesis: for f being Morphism of ,
for g being Morphism of ,
for f' being Morphism of ,
for g' being Morphism of , st f' = f & g' = g holds
f' * g' = g * f
let f be Morphism of ,; :: thesis: for g being Morphism of ,
for f' being Morphism of ,
for g' being Morphism of , st f' = f & g' = g holds
f' * g' = g * f
let g be Morphism of ,; :: thesis: for f' being Morphism of ,
for g' being Morphism of , st f' = f & g' = g holds
f' * g' = g * f
let f' be Morphism of ,; :: thesis: for g' being Morphism of , st f' = f & g' = g holds
f' * g' = g * f
let g' be Morphism of ,; :: thesis: ( f' = f & g' = g implies f' * g' = g * f )
assume that
A17: f' = f and
A18: g' = g ; :: thesis: f' * g' = g * f
thus f' * g' = (the Comp of C . a,b,c) . g,f by A9, A10, A11, A12, A13, A14, A15, A16, A17, A18
.= g * f by A15, A16, ALTCAT_1:def 10 ; :: thesis: verum

end;

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