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
set t = sup 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)) )
A3: 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 A4: 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:35;
then s >= d . ti by A4;
hence ti <= g . s by A1, Th8; :: thesis: verum
end;
then g . s >= sup X by A2, YELLOW_0:30;
hence d . (sup X) <= s by A1, Th8; :: thesis: verum
end;
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) )
assume s in d .: X ; :: thesis: s <= d . (sup X)
then consider ti being Element of T such that
A5: ti in X and
A6: s = d . ti by FUNCT_2:65;
A7: d is monotone by A1, Th8;
reconsider ti = ti as Element of T ;
sup X is_>=_than X by A2, YELLOW_0:30;
then sup X >= ti by A5;
hence s <= d . (sup X) by A7, A6; :: thesis: verum
end;
hence ( ex_sup_of d .: X,S & "\/" ((d .: X),S) = d . ("\/" (X,T)) ) by A3, YELLOW_0:30; :: thesis: verum