let S, T be non empty Poset; :: thesis: for g being Function of S,T st g is upper_adjoint holds
g is infs-preserving
let g be Function of S,T; :: thesis: ( g is upper_adjoint implies g is infs-preserving )
given d being Function of T,S such that A1: [g,d] is Galois ; :: according to WAYBEL_1:def 11 :: thesis: g is infs-preserving
let X be Subset of S; :: according to WAYBEL_0:def 32 :: thesis: g preserves_inf_of X
set s = inf X;
assume A2: ex_inf_of X,S ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of g .: X,T & "/\" ((g .: X),T) = g . ("/\" (X,S)) )
A3: for t being Element of T st t is_<=_than g .: X holds
g . (inf X) >= t
proof
let t be Element of T; :: thesis: ( t is_<=_than g .: X implies g . (inf X) >= t )
assume A4: t is_<=_than g .: X ; :: thesis: g . (inf X) >= t
d . t is_<=_than X
proof
let si be Element of S; :: according to LATTICE3:def 8 :: thesis: ( not si in X or d . t <= si )
assume si in X ; :: thesis: d . t <= si
then g . si in g .: X by FUNCT_2:35;
then t <= g . si by A4;
hence d . t <= si by A1, Th8; :: thesis: verum
end;
then d . t <= inf X by A2, YELLOW_0:31;
hence g . (inf X) >= t by A1, Th8; :: thesis: verum
end;
g . (inf X) is_<=_than g .: X
proof
let t be Element of T; :: according to LATTICE3:def 8 :: thesis: ( not t in g .: X or g . (inf X) <= t )
assume t in g .: X ; :: thesis: g . (inf X) <= t
then consider si being Element of S such that
A5: si in X and
A6: t = g . si by FUNCT_2:65;
A7: g is monotone by A1, Th8;
reconsider si = si as Element of S ;
inf X is_<=_than X by A2, YELLOW_0:31;
then inf X <= si by A5;
hence g . (inf X) <= t by A7, A6; :: thesis: verum
end;
hence ( ex_inf_of g .: X,T & "/\" ((g .: X),T) = g . ("/\" (X,S)) ) by A3, YELLOW_0:31; :: thesis: verum