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