let S, T be complete LATTICE; :: thesis: for g being infs-preserving Function of S,T
for t being Element of T holds (LowerAdj g) . t = inf (g " (uparrow t))
let g be infs-preserving Function of S,T; :: thesis: for t being Element of T holds (LowerAdj g) . t = inf (g " (uparrow t))
let t be Element of T; :: thesis: (LowerAdj g) . t = inf (g " (uparrow t))
[g,(LowerAdj g)] is Galois by Def1;
then (LowerAdj g) . t is_minimum_of g " (uparrow t) by WAYBEL_1:11;
hence (LowerAdj g) . t = inf (g " (uparrow t)) by WAYBEL_1:def 6; :: thesis: verum