[(UpperAdj d),d] is Galois by Def2;
then [(d opp ),((UpperAdj d) opp )] is Galois by YELLOW_7:44;
hence d opp is upper_adjoint by WAYBEL_1:def 11; :: thesis: verum