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