let S, T be non empty Poset; :: thesis: for d being Function of T,S st d is lower_adjoint holds
d is sups-preserving
let d be Function of T,S; :: thesis: ( d is lower_adjoint implies d is sups-preserving )
given g being Function of S,T such that A1: [g,d] is Galois ; :: according to WAYBEL_1:def 12 :: thesis: d is sups-preserving
let X be Subset of T; :: according to WAYBEL_0:def 33 :: thesis: d preserves_sup_of X
assume A2: ex_sup_of X,T ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of d .: X,S & "\/" (d .: X),S = d . ("\/" X,T) )
set t = sup X;
A3: d . (sup X) is_>=_than d .: X

proof

let s be Element of S; :: according to LATTICE3:def 9 :: thesis: ( not s in d .: X or s <= d . (sup X) )
A4: d is monotone by A1, Th9;
A5: sup X is_>=_than X by A2, YELLOW_0:30;
assume s in d .: X ; :: thesis: s <= d . (sup X)
then consider ti being Element of T such that
A6: ti in X and
A7: s = d . ti by FUNCT_2:116;
reconsider ti = ti as Element of T ;
sup X >= ti by A5, A6, LATTICE3:def 9;
hence d . (sup X) >= s by A4, A7, Def2; :: thesis: verum

end;

for s being Element of S st s is_>=_than d .: X holds
d . (sup X) <= s

proof

let s be Element of S; :: thesis: ( s is_>=_than d .: X implies d . (sup X) <= s )
assume A8: s is_>=_than d .: X ; :: thesis: d . (sup X) <= s
g . s is_>=_than X

proof

let ti be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not ti in X or ti <= g . s )
assume ti in X ; :: thesis: ti <= g . s
then d . ti in d .: X by FUNCT_2:43;
then s >= d . ti by A8, LATTICE3:def 9;
hence g . s >= ti by A1, Th9; :: thesis: verum

end;

then g . s >= sup X by A2, YELLOW_0:30;
hence d . (sup X) <= s by A1, Th9; :: thesis: verum

end;

hence ( ex_sup_of d .: X,S & "\/" (d .: X),S = d . ("\/" X,T) ) by A3, YELLOW_0:30; :: thesis: verum