let S, T be complete LATTICE; :: thesis: for d being sups-preserving Function of T,S
for s being Element of S holds (UpperAdj d) . s = sup (d " (downarrow s))
let d be sups-preserving Function of T,S; :: thesis: for s being Element of S holds (UpperAdj d) . s = sup (d " (downarrow s))
let s be Element of S; :: thesis: (UpperAdj d) . s = sup (d " (downarrow s))
[(UpperAdj d),d] is Galois by Def2;
then (UpperAdj d) . s is_maximum_of d " (downarrow s) by WAYBEL_1:11;
hence (UpperAdj d) . s = sup (d " (downarrow s)) by WAYBEL_1:def 7; :: thesis: verum