let A, B be non empty AltCatStr ; :: thesis: ( A,B are_opposite implies for a, b being object of
for a', b' being object of st a' = a & b' = b holds
<^a,b^> = <^b',a'^> )
assume that
the carrier of B = the carrier of A and
A1: the Arrows of B = ~ the Arrows of A ; :: according to YELLOW18:def 3 :: thesis: ( ex a, b, c being object of ex a', b', c' being object of st
( a' = a & b' = b & c' = c & not the Comp of B . a',b',c' = ~ (the Comp of A . c,b,a) ) or for a, b being object of
for a', b' being object of st a' = a & b' = b holds
<^a,b^> = <^b',a'^> )
assume for a, b, c being object of
for a', b', c' being object of st a' = a & b' = b & c' = c holds
the Comp of B . a',b',c' = ~ (the Comp of A . c,b,a) ; :: thesis: for a, b being object of
for a', b' being object of st a' = a & b' = b holds
<^a,b^> = <^b',a'^>
let a, b be object of ; :: thesis: for a', b' being object of st a' = a & b' = b holds
<^a,b^> = <^b',a'^>
let a', b' be object of ; :: thesis: ( a' = a & b' = b implies <^a,b^> = <^b',a'^> )
thus ( a' = a & b' = b implies <^a,b^> = <^b',a'^> ) by A1, ALTCAT_2:6; :: thesis: verum