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