let S, T be non empty Poset; :: thesis: for d being Function of T,S st T is complete holds
( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) )
let d be Function of T,S; :: thesis: ( T is complete implies ( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) ) )
assume A1: T is complete ; :: thesis: ( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) )
hereby :: thesis: ( d is monotone & d is lower_adjoint implies d is sups-preserving )
assume d is sups-preserving ; :: thesis: ( d is monotone & d is lower_adjoint )
then ex g being Function of S,T st
( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) by A1, Th15;
hence ( d is monotone & d is lower_adjoint ) by Th11; :: thesis: verum
end;
assume d is monotone ; :: thesis: ( not d is lower_adjoint or d is sups-preserving )
assume ex g being Function of S,T st [g,d] is Galois ; :: according to WAYBEL_1:def 12 :: thesis: d is sups-preserving
then d is lower_adjoint ;
hence d is sups-preserving ; :: thesis: verum