theorem :: WAYBEL34:3

for S, T being complete LATTICE
for d being sups-preserving Function of T,S
for s being Element of S holds (UpperAdj d) . s = sup (d " (downarrow s))