[(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 ; :: thesis: verum