let A, B, A', B' be category; :: thesis: for F being FunctorStr of A,B st A',B' are_anti-isomorphic_under F holds
A',B' are_anti-isomorphic
let F be FunctorStr of A,B; :: thesis: ( A',B' are_anti-isomorphic_under F implies A',B' are_anti-isomorphic )
assume ( A' is subcategory of A & B' is subcategory of B ) ; :: according to YELLOW20:def 5 :: thesis: ( for G being contravariant Functor of A',B' holds
( not G is bijective or ex a' being object of A' ex a being object of A st
( a' = a & not G . a' = F . a ) or ex b', c' being object of A' ex b, c being object of A st
( <^b',c'^> <> {} & b' = b & c' = c & ex f' being Morphism of b',c' ex f being Morphism of b,c st
( f' = f & not G . f' = (Morph-Map F,b,c) . f ) ) ) or A',B' are_anti-isomorphic )
given G being contravariant Functor of A',B' such that A1: G is bijective and
( ( for a' being object of A'
for a being object of A st a' = a holds
G . a' = F . a ) & ( for b', c' being object of A'
for b, c being object of A st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c st f' = f holds
G . f' = (Morph-Map F,b,c) . f ) ) ; :: thesis: A',B' are_anti-isomorphic
take G ; :: according to FUNCTOR0:def 41 :: thesis: ( G is bijective & G is contravariant )
thus ( G is bijective & G is contravariant ) by A1; :: thesis: verum