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