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 10;
A2: 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 )
A3: (W LowerAdj) . a = latt a by Def6;
A4: 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 Th48;
hence ( a is Object of B1 iff (W LowerAdj) . a is Object of B2 ) by A3, A4, Th50; :: thesis: verum

end;

A5: now :: thesis: for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
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 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 A6: <^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 that
A7: a1 = a and
A8: 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 that
A9: a2 = (W LowerAdj) . a and
A10: 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^> ) )
A11: @ f = f by A6, YELLOW21:def 7;
A12: (W LowerAdj) . a = latt a by Def6;
A13: (W LowerAdj) . b = latt b by Def6;
A14: (W LowerAdj) . f = LowerAdj (@ f) by A6, Def6;
reconsider g = f as infs-preserving Function of (latt a1),(latt b1) by A1, A6, A7, A8, A11, Def4;
A15: UpperAdj (LowerAdj g) = g by Th10;
then ( f in <^a1,b1^> iff UpperAdj (LowerAdj g) is directed-sups-preserving ) by Th49;
hence ( f in <^a1,b1^> implies (W LowerAdj) . f in <^b2,a2^> ) by A7, A8, A9, A10, A11, A12, A13, A14, Th51; :: 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 Th51;
hence f in <^a1,b1^> by A7, A8, A9, A10, A11, A12, A13, A14, A15, Th49; :: thesis: verum

end;

B1,B2 are_anti-isomorphic_under W LowerAdj by A2, A5, YELLOW20:57;
hence W -CL_category ,W -CL-opp_category are_anti-isomorphic_under W LowerAdj ; :: thesis: verum