let S, T be non empty Poset; :: thesis: for g being Function of S,T st S is complete holds
( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) )
let g be Function of S,T; :: thesis: ( S is complete implies ( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) ) )
assume A1: S is complete ; :: thesis: ( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) )

hereby :: thesis: ( g is monotone & g is upper_adjoint implies g is infs-preserving )

assume g is infs-preserving ; :: thesis: ( g is monotone & g is upper_adjoint )
then ex d being Function of T,S st
( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) by A1, Th14;
hence ( g is monotone & g is upper_adjoint ) by Th10; :: thesis: verum

end;

assume g is monotone ; :: thesis: ( not g is upper_adjoint or g is infs-preserving )
assume ex d being Function of T,S st [g,d] is Galois ; :: according to WAYBEL_1:def 11 :: thesis: g is infs-preserving
then g is upper_adjoint ;
hence g is infs-preserving ; :: thesis: verum