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