:: deftheorem Def2 defines UpperAdj WAYBEL34:def 2 :
for S, T being LATTICE
for d being Function of T,S st T is complete & d is sups-preserving holds
for b₄ being Function of S,T holds
( b₄ = UpperAdj d iff [b₄,d] is Galois );