let S, T be complete LATTICE; :: thesis: for g being infs-preserving Function of S,T st g is directed-sups-preserving holds
LowerAdj g is waybelow-preserving
let g be infs-preserving Function of S,T; :: thesis: ( g is directed-sups-preserving implies LowerAdj g is waybelow-preserving )
assume A1: g is directed-sups-preserving ; :: thesis: LowerAdj g is waybelow-preserving
set d = LowerAdj g;
A2: [g,(LowerAdj g)] is Galois by Def1;
let t, t9 be Element of T; :: according to WAYBEL34:def 8 :: thesis: ( t << t9 implies (LowerAdj g) . t << (LowerAdj g) . t9 )
assume A3: t << t9 ; :: thesis: (LowerAdj g) . t << (LowerAdj g) . t9
let D be non empty directed Subset of S; :: according to WAYBEL_3:def 1 :: thesis: ( not (LowerAdj g) . t9 <= "\/" (D,S) or ex b₁ being Element of the carrier of S st
( b₁ in D & (LowerAdj g) . t <= b₁ ) )
assume (LowerAdj g) . t9 <= sup D ; :: thesis: ex b₁ being Element of the carrier of S st
( b₁ in D & (LowerAdj g) . t <= b₁ )
then A4: t9 <= g . (sup D) by A2, WAYBEL_1:8;
A5: g preserves_sup_of D by A1;
ex_sup_of D,S by YELLOW_0:17;
then A6: g . (sup D) = sup (g .: D) by A5;
( g .: D is directed & not g .: D is empty ) by YELLOW_2:15;
then consider x being Element of T such that
A7: x in g .: D and
A8: t <= x by A3, A4, A6;
consider s being object such that
A9: s in the carrier of S and
A10: s in D and
A11: x = g . s by A7, FUNCT_2:64;
reconsider s = s as Element of S by A9;
take s ; :: thesis: ( s in D & (LowerAdj g) . t <= s )
thus ( s in D & (LowerAdj g) . t <= s ) by A2, A8, A10, A11, WAYBEL_1:8; :: thesis: verum