let W be with_non-empty_element set ; :: thesis: W -CL_category ,W -CL-opp_category are_anti-isomorphic_under W LowerAdj
set A1 = W -INF_category ;
set A2 = W -SUP_category ;
reconsider B1 = W -CL_category as non empty subcategory of W -INF_category by ALTCAT_4:36;
reconsider B2 = W -CL-opp_category as non empty subcategory of W -SUP_category by ALTCAT_4:36;
set F = W LowerAdj ;
A1: ex a being non empty set st a in W by SETFAM_1:def 11;
A2: W LowerAdj is bijective ;
A3: for a being object of (W -INF_category ) holds
( a is object of B1 iff (W LowerAdj ) . a is object of B2 )

proof

let a be object of (W -INF_category ); :: thesis: ( a is object of B1 iff (W LowerAdj ) . a is object of B2 )
A4: ( latt a = a & (W LowerAdj ) . a = latt a ) by Def6;
A5: the carrier of (latt a) in W by A1, Def4;
then ( a is object of B1 iff ( latt a is strict & latt a is complete & latt a is continuous ) ) by Th52;
hence ( a is object of B1 iff (W LowerAdj ) . a is object of B2 ) by A4, A5, Th54; :: thesis: verum

end;

A6: now

let a, b be object of (W -INF_category ); :: thesis: ( <^a,b^> <> {} implies for a1, b1 being object of B1 st a1 = a & b1 = b holds
for a2, b2 being object of B2 st a2 = (W LowerAdj ) . a & b2 = (W LowerAdj ) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj ) . f in <^b2,a2^> ) & ( (W LowerAdj ) . f in <^b2,a2^> implies f in <^a1,b1^> ) ) )
assume A7: <^a,b^> <> {} ; :: thesis: for a1, b1 being object of B1 st a1 = a & b1 = b holds
for a2, b2 being object of B2 st a2 = (W LowerAdj ) . a & b2 = (W LowerAdj ) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj ) . f in <^b2,a2^> ) & ( (W LowerAdj ) . f in <^b2,a2^> implies f in <^a1,b1^> ) )
let a1, b1 be object of B1; :: thesis: ( a1 = a & b1 = b implies for a2, b2 being object of B2 st a2 = (W LowerAdj ) . a & b2 = (W LowerAdj ) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj ) . f in <^b2,a2^> ) & ( (W LowerAdj ) . f in <^b2,a2^> implies f in <^a1,b1^> ) ) )
assume A8: ( a1 = a & b1 = b ) ; :: thesis: for a2, b2 being object of B2 st a2 = (W LowerAdj ) . a & b2 = (W LowerAdj ) . b holds
for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj ) . f in <^b2,a2^> ) & ( (W LowerAdj ) . f in <^b2,a2^> implies f in <^a1,b1^> ) )
let a2, b2 be object of B2; :: thesis: ( a2 = (W LowerAdj ) . a & b2 = (W LowerAdj ) . b implies for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj ) . f in <^b2,a2^> ) & ( (W LowerAdj ) . f in <^b2,a2^> implies f in <^a1,b1^> ) ) )
assume A9: ( a2 = (W LowerAdj ) . a & b2 = (W LowerAdj ) . b ) ; :: thesis: for f being Morphism of a,b holds
( ( f in <^a1,b1^> implies (W LowerAdj ) . f in <^b2,a2^> ) & ( (W LowerAdj ) . f in <^b2,a2^> implies f in <^a1,b1^> ) )
let f be Morphism of a,b; :: thesis: ( ( f in <^a1,b1^> implies (W LowerAdj ) . f in <^b2,a2^> ) & ( (W LowerAdj ) . f in <^b2,a2^> implies f in <^a1,b1^> ) )
<^((W LowerAdj ) . b),((W LowerAdj ) . a)^> <> {} by A7, FUNCTOR0:def 20;
then A10: ( @ f = f & @ ((W LowerAdj ) . f) = (W LowerAdj ) . f & latt a1 = a1 & latt b1 = b1 & latt a = a & latt b = b & latt a2 = a2 & latt b2 = b2 ) by A7, YELLOW21:def 7;
then A11: ( (W LowerAdj ) . a = latt a & (W LowerAdj ) . b = latt b & (W LowerAdj ) . f = LowerAdj (@ f) & @ f is infs-preserving ) by A1, A7, Def4, Def6;
reconsider g = f as infs-preserving Function of (latt a1),(latt b1) by A1, A7, A8, A10, Def4;
A12: UpperAdj (LowerAdj g) = g by Th10;
then ( f in <^a1,b1^> iff UpperAdj (LowerAdj g) is directed-sups-preserving ) by Th53;
hence ( f in <^a1,b1^> implies (W LowerAdj ) . f in <^b2,a2^> ) by A8, A9, A10, A11, Th55; :: thesis: ( (W LowerAdj ) . f in <^b2,a2^> implies f in <^a1,b1^> )
assume (W LowerAdj ) . f in <^b2,a2^> ; :: thesis: f in <^a1,b1^>
then ex g being sups-preserving Function of (latt b2),(latt a2) st
( (W LowerAdj ) . f = g & UpperAdj g is directed-sups-preserving ) by Th55;
hence f in <^a1,b1^> by A8, A9, A10, A11, A12, Th53; :: thesis: verum

end;

B1,B2 are_anti-isomorphic_under W LowerAdj from YELLOW20:sch 5(A2, A3, A6);
hence W -CL_category ,W -CL-opp_category are_anti-isomorphic_under W LowerAdj ; :: thesis: verum