[g,(LowerAdj g)] is Galois by Def1;
then [((LowerAdj g) opp),(g opp)] is Galois by YELLOW_7:44;
hence g opp is lower_adjoint ; :: thesis: verum