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