let W be with_non-empty_element set ; :: thesis: W -INF(SC)_category ,W -SUP(SO)_category are_anti-isomorphic_under W LowerAdj
set A1 = W -INF_category ;
set B1 = W -INF(SC)_category ;
set B2 = W -SUP(SO)_category ;
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 (W -INF(SC)_category) iff (W LowerAdj) . a is Object of (W -SUP(SO)_category) ) by Def10, Def11;

A3: now :: thesis: for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for a1, b1 being Object of (W -INF(SC)_category) st a1 = a & b1 = b holds
for a2, b2 being Object of (W -SUP(SO)_category) st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> )

let a, b be Object of (W -INF_category); :: thesis: ( <^a,b^> <> {} implies for a1, b1 being Object of (W -INF(SC)_category) st a1 = a & b1 = b holds
for a2, b2 being Object of (W -SUP(SO)_category) st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> ) )
assume A4: <^a,b^> <> {} ; :: thesis: for a1, b1 being Object of (W -INF(SC)_category) st a1 = a & b1 = b holds
for a2, b2 being Object of (W -SUP(SO)_category) st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> )
let a1, b1 be Object of (W -INF(SC)_category); :: thesis: ( a1 = a & b1 = b implies for a2, b2 being Object of (W -SUP(SO)_category) st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> ) )
assume that
A5: a1 = a and
A6: b1 = b ; :: thesis: for a2, b2 being Object of (W -SUP(SO)_category) st a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b holds
for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> )
let a2, b2 be Object of (W -SUP(SO)_category); :: thesis: ( a2 = (W LowerAdj) . a & b2 = (W LowerAdj) . b implies for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> ) )
assume that
A7: a2 = (W LowerAdj) . a and
A8: b2 = (W LowerAdj) . b ; :: thesis: for f being Morphism of a,b holds
( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> )
let f be Morphism of a,b; :: thesis: ( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> )
A9: <^((W LowerAdj) . b),((W LowerAdj) . a)^> <> {} by A4, FUNCTOR0:def 19;
A10: @ f = f by A4, YELLOW21:def 7;
A11: @ ((W LowerAdj) . f) = (W LowerAdj) . f by A9, 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 A4, Def6;
reconsider g = f as infs-preserving Function of (latt a1),(latt b1) by A1, A4, A5, A6, A10, Def4;
UpperAdj (LowerAdj g) = g by Th10;
then ( f in <^a1,b1^> iff UpperAdj (LowerAdj g) is directed-sups-preserving ) by A4, A5, A6, A10, Def10;
hence ( f in <^a1,b1^> iff (W LowerAdj) . f in <^b2,a2^> ) by A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Def11; :: thesis: verum

end;

thus W -INF(SC)_category ,W -SUP(SO)_category are_anti-isomorphic_under W LowerAdj by A2, A3, YELLOW20:57; :: thesis: verum