:: deftheorem Def1 defines LowerAdj WAYBEL34:def 1 :
for S, T being LATTICE
for g being Function of S,T st S is complete & g is infs-preserving holds
for b₄ being Function of T,S holds
( b₄ = LowerAdj g iff [g,b₄] is Galois );