let W be with_non-empty_element set ; :: thesis: ( (W LowerAdj) " = W UpperAdj & (W UpperAdj) " = W LowerAdj )
A1: ex x being non empty set st x in W by SETFAM_1:def 10;
set B = W -SUP_category ;
set F = W LowerAdj ;
set G = W UpperAdj ;

A2: now :: thesis: for a being Object of (W -SUP_category) holds (W LowerAdj) . ((W UpperAdj) . a) = a

let a be Object of (W -SUP_category); :: thesis: (W LowerAdj) . ((W UpperAdj) . a) = a
thus (W LowerAdj) . ((W UpperAdj) . a) = latt ((W UpperAdj) . a) by Def6
.= latt a by Def7
.= a ; :: thesis: verum

end;

now :: thesis: for a, b being Object of (W -SUP_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds (W LowerAdj) . ((W UpperAdj) . f) = f

let a, b be Object of (W -SUP_category); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (W LowerAdj) . ((W UpperAdj) . f) = f )
assume A3: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds (W LowerAdj) . ((W UpperAdj) . f) = f
then A4: <^((W UpperAdj) . b),((W UpperAdj) . a)^> <> {} by FUNCTOR0:def 19;
let f be Morphism of a,b; :: thesis: (W LowerAdj) . ((W UpperAdj) . f) = f
A5: (W UpperAdj) . f = UpperAdj (@ f) by A3, Def7;
A6: @ f = f by A3, YELLOW21:def 7;
A7: @ ((W UpperAdj) . f) = (W UpperAdj) . f by A4, YELLOW21:def 7;
A8: (W UpperAdj) . a = latt a by Def7;
A9: (W UpperAdj) . b = latt b by Def7;
A10: @ f is sups-preserving by A1, A3, A6, Def5;
thus (W LowerAdj) . ((W UpperAdj) . f) = LowerAdj (@ ((W UpperAdj) . f)) by A4, Def6
.= f by A5, A6, A7, A8, A9, A10, Th11 ; :: thesis: verum

end;

hence (W LowerAdj) " = W UpperAdj by A2, YELLOW20:7; :: thesis: (W UpperAdj) " = W LowerAdj
set B = W -INF_category ;
set G = W LowerAdj ;
set F = W UpperAdj ;

A11: now :: thesis: for a being Object of (W -INF_category) holds (W UpperAdj) . ((W LowerAdj) . a) = a

let a be Object of (W -INF_category); :: thesis: (W UpperAdj) . ((W LowerAdj) . a) = a
thus (W UpperAdj) . ((W LowerAdj) . a) = latt ((W LowerAdj) . a) by Def7
.= latt a by Def6
.= a ; :: thesis: verum

end;

now :: thesis: for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds (W UpperAdj) . ((W LowerAdj) . f) = f

let a, b be Object of (W -INF_category); :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (W UpperAdj) . ((W LowerAdj) . f) = f )
assume A12: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds (W UpperAdj) . ((W LowerAdj) . f) = f
then A13: <^((W LowerAdj) . b),((W LowerAdj) . a)^> <> {} by FUNCTOR0:def 19;
let f be Morphism of a,b; :: thesis: (W UpperAdj) . ((W LowerAdj) . f) = f
A14: (W LowerAdj) . f = LowerAdj (@ f) by A12, Def6;
A15: @ f = f by A12, YELLOW21:def 7;
A16: @ ((W LowerAdj) . f) = (W LowerAdj) . f by A13, YELLOW21:def 7;
A17: (W LowerAdj) . a = latt a by Def6;
A18: (W LowerAdj) . b = latt b by Def6;
A19: @ f is infs-preserving by A1, A12, A15, Def4;
thus (W UpperAdj) . ((W LowerAdj) . f) = UpperAdj (@ ((W LowerAdj) . f)) by A13, Def7
.= f by A14, A15, A16, A17, A18, A19, Th10 ; :: thesis: verum

end;

hence (W UpperAdj) " = W LowerAdj by A11, YELLOW20:7; :: thesis: verum