let S, T be complete LATTICE; :: thesis: for g being infs-preserving Function of S,T holds LowerAdj g = UpperAdj (g opp)
let g be infs-preserving Function of S,T; :: thesis: LowerAdj g = UpperAdj (g opp)
[g,(LowerAdj g)] is Galois by Def1;
then [((LowerAdj g) opp),(g opp)] is Galois by YELLOW_7:44;
hence LowerAdj g = UpperAdj (g opp) by Def2; :: thesis: verum