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