let A1, A2 be category; :: thesis: for F being contravariant Functor of A1,A2 st F is bijective holds
for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds
B2,B1 are_anti-isomorphic_under F "
let F be contravariant Functor of A1,A2; :: thesis: ( F is bijective implies for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds
B2,B1 are_anti-isomorphic_under F " )
assume A1: F is bijective ; :: thesis: for B1 being non empty subcategory of A1
for B2 being non empty subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds
B2,B1 are_anti-isomorphic_under F "
let B1 be non empty subcategory of A1; :: thesis: for B2 being non empty subcategory of A2 st B1,B2 are_anti-isomorphic_under F holds
B2,B1 are_anti-isomorphic_under F "
let B2 be non empty subcategory of A2; :: thesis: ( B1,B2 are_anti-isomorphic_under F implies B2,B1 are_anti-isomorphic_under F " )
assume ( B1 is subcategory of A1 & B2 is subcategory of A2 ) ; :: according to YELLOW20:def 5 :: thesis: ( for G being contravariant Functor of B1,B2 holds
( not G is bijective or ex a' being object of B1 ex a being object of A1 st
( a' = a & not G . a' = F . a ) or ex b', c' being object of B1 ex b, c being object of A1 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 B2,B1 are_anti-isomorphic_under F " )
given G being contravariant Functor of B1,B2 such that A2: G is bijective and
A3: for a being object of B1
for a1 being object of A1 st a = a1 holds
G . a = F . a1 and
A4: for b, c being object of B1
for b1, c1 being object of A1 st <^b,c^> <> {} & b = b1 & c = c1 holds
for f being Morphism of b,c
for f1 being Morphism of b1,c1 st f = f1 holds
G . f = (Morph-Map F,b1,c1) . f1 ; :: thesis: B2,B1 are_anti-isomorphic_under F "
thus ( B2 is subcategory of A2 & B1 is subcategory of A1 ) ; :: according to YELLOW20:def 5 :: thesis: ex G being contravariant Functor of B2,B1 st
( G is bijective & ( for a' being object of B2
for a being object of A2 st a' = a holds
G . a' = (F " ) . a ) & ( for b', c' being object of B2
for b, c being object of A2 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 ) )
consider H being Functor of B2,B1 such that
A5: ( H = G " & H is bijective & H is contravariant ) by A2, FUNCTOR0:50;
reconsider H = H as contravariant Functor of B2,B1 by A5;
ex H being Functor of A2,A1 st
( H = F " & H is bijective & H is contravariant ) by A1, FUNCTOR0:50;
then reconsider F' = F " as contravariant Functor of A2,A1 ;
take H ; :: thesis: ( H is bijective & ( for a' being object of B2
for a being object of A2 st a' = a holds
H . a' = (F " ) . a ) & ( for b', c' being object of B2
for b, c being object of A2 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
H . f' = (Morph-Map (F " ),b,c) . f ) )
thus H is bijective by A5; :: thesis: ( ( for a' being object of B2
for a being object of A2 st a' = a holds
H . a' = (F " ) . a ) & ( for b', c' being object of B2
for b, c being object of A2 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
H . f' = (Morph-Map (F " ),b,c) . f ) )
A6: ( the carrier of B1 c= the carrier of A1 & the carrier of B2 c= the carrier of A2 ) by ALTCAT_2:def 11;
( F is surjective & G is surjective ) by A1, A2, FUNCTOR0:def 36;
then ( F is onto & G is onto ) by FUNCTOR0:def 35;
then A7: ( F is coreflexive & G is coreflexive ) by FUNCTOR0:48;

hereby :: thesis: for b', c' being object of B2
for b, c being object of A2 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
H . f' = (Morph-Map (F " ),b,c) . f

let a be object of B2; :: thesis: for a1 being object of A2 st a = a1 holds
H . a = (F " ) . a1
let a1 be object of A2; :: thesis: ( a = a1 implies H . a = (F " ) . a1 )
H . a in the carrier of B1 ;
then reconsider Ha = H . a as object of A1 by A6;
assume A9: a = a1 ; :: thesis: H . a = (F " ) . a1
G . (H . a) = F . Ha by A3;
then F . Ha = a by A2, A5, A7, Th1;
hence H . a = (F " ) . a1 by A1, A7, A9, Th1; :: thesis: verum

end;

let b, c be object of B2; :: thesis: for b, c being object of A2 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
H . f' = (Morph-Map (F " ),b,c) . f
let b1, c1 be object of A2; :: thesis: ( <^b,c^> <> {} & b = b1 & c = c1 implies for f' being Morphism of b,c
for f being Morphism of b1,c1 st f' = f holds
H . f' = (Morph-Map (F " ),b1,c1) . f )
assume A10: ( <^b,c^> <> {} & b = b1 & c = c1 ) ; :: thesis: for f' being Morphism of b,c
for f being Morphism of b1,c1 st f' = f holds
H . f' = (Morph-Map (F " ),b1,c1) . f
let f be Morphism of b,c; :: thesis: for f being Morphism of b1,c1 st f = f holds
H . f = (Morph-Map (F " ),b1,c1) . f
let f1 be Morphism of b1,c1; :: thesis: ( f = f1 implies H . f = (Morph-Map (F " ),b1,c1) . f1 )
assume A11: f = f1 ; :: thesis: H . f = (Morph-Map (F " ),b1,c1) . f1
A12: ( H . b = (F " ) . b1 & H . c = (F " ) . c1 & <^(H . c),(H . b)^> <> {} ) by A8, A10, FUNCTOR0:def 20;
then A13: ( <^(H . c),(H . b)^> c= <^((F " ) . c1),((F " ) . b1)^> & H . f in <^(H . c),(H . b)^> ) by ALTCAT_2:32;
then reconsider Hf = H . f as Morphism of ((F " ) . c1),((F " ) . b1) ;
A14: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A10, ALTCAT_2:32;
then A15: ( F . ((F " ) . b1) = b1 & F . ((F " ) . c1) = c1 & f in <^b1,c1^> ) by A1, A7, Th1;
A16: ( G . (H . b) = b & G . (H . c) = c ) by A2, A5, A7, Th1;
G . (H . f) = (Morph-Map F,((F " ) . c1),((F " ) . b1)) . Hf by A4, A12
.= F . Hf by A13, A15, FUNCTOR0:def 17 ;
then F . Hf = f by A2, A5, A12, A16, Th3;
hence H . f = F' . f1 by A1, A11, A13, A15, Th3
.= (Morph-Map (F " ),b1,c1) . f1 by A13, A14, FUNCTOR0:def 17 ;
:: thesis: verum