:: deftheorem Def12 defines lower_adjoint WAYBEL_1:def 12 :
for S, T being non empty RelStr
for d being Function of T,S holds
( d is lower_adjoint iff ex g being Function of S,T st [g,d] is Galois );