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 11;
set B = W -SUP_category ;
set F = W LowerAdj ;
set G = W UpperAdj ;

A2: now

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

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 20;
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 & @ ((W UpperAdj ) . f) = (W UpperAdj ) . f ) by A3, A4, YELLOW21:def 7;
A7: ( latt ((W UpperAdj ) . a) = (W UpperAdj ) . a & latt ((W UpperAdj ) . b) = (W UpperAdj ) . b & latt a = a & latt b = b & (W UpperAdj ) . a = latt a & (W UpperAdj ) . b = latt b ) by Def7;
A8: ( latt a is complete & latt b is complete & @ 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, 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 ;

A9: now

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

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 A10: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds (W UpperAdj ) . ((W LowerAdj ) . f) = f
then A11: <^((W LowerAdj ) . b),((W LowerAdj ) . a)^> <> {} by FUNCTOR0:def 20;
let f be Morphism of a,b; :: thesis: (W UpperAdj ) . ((W LowerAdj ) . f) = f
A12: (W LowerAdj ) . f = LowerAdj (@ f) by A10, Def6;
A13: ( @ f = f & @ ((W LowerAdj ) . f) = (W LowerAdj ) . f ) by A10, A11, YELLOW21:def 7;
A14: ( latt ((W LowerAdj ) . a) = (W LowerAdj ) . a & latt ((W LowerAdj ) . b) = (W LowerAdj ) . b & latt a = a & latt b = b & (W LowerAdj ) . a = latt a & (W LowerAdj ) . b = latt b ) by Def6;
A15: ( latt a is complete & latt b is complete & @ f is infs-preserving ) by A1, A10, A13, Def4;
thus (W UpperAdj ) . ((W LowerAdj ) . f) = UpperAdj (@ ((W LowerAdj ) . f)) by A11, Def7
.= f by A12, A13, A14, A15, Th10 ; :: thesis: verum

end;

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