let A be category; :: thesis: for B being non empty subcategory of non empty holds B,B opp are_anti-isomorphic_under dualizing-func A,(A opp )
let B be non empty subcategory of non empty ; :: thesis: B,B opp are_anti-isomorphic_under dualizing-func A,(A opp )
set F = dualizing-func A,(A opp );
A1: B,B opp are_opposite by YELLOW18:def 4;
thus ( B is subcategory of & B opp is subcategory of ) by Th49; :: according to YELLOW20:def 5 :: thesis: ex G being contravariant Functor of B,B opp st
( G is bijective & ( for a' being object of
for a being object of st a' = a holds
G . a' = (dualizing-func A,(A opp )) . a ) & ( for b', c' being object of
for b, c being object of st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of ,
for f being Morphism of , st f' = f holds
G . f' = (Morph-Map (dualizing-func A,(A opp )),b,c) . f ) )
take G = dualizing-func B,(B opp ); :: thesis: ( G is bijective & ( for a' being object of
for a being object of st a' = a holds
G . a' = (dualizing-func A,(A opp )) . a ) & ( for b', c' being object of
for b, c being object of st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of ,
for f being Morphism of , st f' = f holds
G . f' = (Morph-Map (dualizing-func A,(A opp )),b,c) . f ) )
thus G is bijective ; :: thesis: ( ( for a' being object of
for a being object of st a' = a holds
G . a' = (dualizing-func A,(A opp )) . a ) & ( for b', c' being object of
for b, c being object of st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of ,
for f being Morphism of , st f' = f holds
G . f' = (Morph-Map (dualizing-func A,(A opp )),b,c) . f ) )
A2: A,A opp are_opposite by YELLOW18:def 4;

hereby :: thesis: for b', c' being object of
for b, c being object of st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of ,
for f being Morphism of , st f' = f holds
G . f' = (Morph-Map (dualizing-func A,(A opp )),b,c) . f

let a be object of ; :: thesis: for a1 being object of st a = a1 holds
G . a = (dualizing-func A,(A opp )) . a1
let a1 be object of ; :: thesis: ( a = a1 implies G . a = (dualizing-func A,(A opp )) . a1 )
assume a = a1 ; :: thesis: G . a = (dualizing-func A,(A opp )) . a1
hence G . a = a1 by A1, YELLOW18:def 5
.= (dualizing-func A,(A opp )) . a1 by A2, YELLOW18:def 5 ;
:: thesis: verum

end;

let b, c be object of ; :: thesis: for b, c being object of st <^b,c^> <> {} & b = b & c = c holds
for f' being Morphism of ,
for f being Morphism of , st f' = f holds
G . f' = (Morph-Map (dualizing-func A,(A opp )),b,c) . f
let b1, c1 be object of ; :: thesis: ( <^b,c^> <> {} & b = b1 & c = c1 implies for f' being Morphism of ,
for f being Morphism of , st f' = f holds
G . f' = (Morph-Map (dualizing-func A,(A opp )),b1,c1) . f )
assume that
A3: <^b,c^> <> {} and
A4: ( b = b1 & c = c1 ) ; :: thesis: for f' being Morphism of ,
for f being Morphism of , st f' = f holds
G . f' = (Morph-Map (dualizing-func A,(A opp )),b1,c1) . f
let f be Morphism of ,; :: thesis: for f being Morphism of , st f = f holds
G . f = (Morph-Map (dualizing-func A,(A opp )),b1,c1) . f
let f1 be Morphism of ,; :: thesis: ( f = f1 implies G . f = (Morph-Map (dualizing-func A,(A opp )),b1,c1) . f1 )
assume A5: f = f1 ; :: thesis: G . f = (Morph-Map (dualizing-func A,(A opp )),b1,c1) . f1
A6: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A3, A4, ALTCAT_2:32;
then A7: <^((dualizing-func A,(A opp )) . c1),((dualizing-func A,(A opp )) . b1)^> <> {} by FUNCTOR0:def 20;
thus G . f = f by A1, A3, YELLOW18:def 5
.= (dualizing-func A,(A opp )) . f1 by A2, A5, A6, YELLOW18:def 5
.= (Morph-Map (dualizing-func A,(A opp )),b1,c1) . f1 by A6, A7, FUNCTOR0:def 17 ; :: thesis: verum