let S be complete LATTICE; :: thesis: for T being continuous complete LATTICE
for g being infs-preserving Function of S,T st LowerAdj g is waybelow-preserving holds
g is directed-sups-preserving
let T be continuous complete LATTICE; :: thesis: for g being infs-preserving Function of S,T st LowerAdj g is waybelow-preserving holds
g is directed-sups-preserving
let g be infs-preserving Function of S,T; :: thesis: ( LowerAdj g is waybelow-preserving implies g is directed-sups-preserving )
assume A1: for t, t' being Element of T st t << t' holds
(LowerAdj g) . t << (LowerAdj g) . t' ; :: according to WAYBEL34:def 8 :: thesis: g is directed-sups-preserving
let D be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( D is empty or not D is directed or g preserves_sup_of D )
assume A2: ( not D is empty & D is directed ) ; :: thesis: g preserves_sup_of D
assume ex_sup_of D,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of g .: D,T & "\/" (g .: D),T = g . ("\/" D,S) )
thus ex_sup_of g .: D,T by YELLOW_0:17; :: thesis: "\/" (g .: D),T = g . ("\/" D,S)
A3: sup (g .: D) <= g . (sup D) by WAYBEL17:15;
A4: g . (sup D) = sup (waybelow (g . (sup D))) by WAYBEL_3:def 5;
waybelow (g . (sup D)) is_<=_than sup (g .: D)

proof

let t be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not t in waybelow (g . (sup D)) or t <= sup (g .: D) )
assume t in waybelow (g . (sup D)) ; :: thesis: t <= sup (g .: D)
then t << g . (sup D) by WAYBEL_3:7;
then A5: (LowerAdj g) . t << (LowerAdj g) . (g . (sup D)) by A1;
A6: [g,(LowerAdj g)] is Galois by Def1;
then ( (LowerAdj g) * g <= id S & (id S) . (sup D) = sup D ) by FUNCT_1:35, WAYBEL_1:19;
then ((LowerAdj g) * g) . (sup D) <= sup D by YELLOW_2:10;
then (LowerAdj g) . (g . (sup D)) <= sup D by FUNCT_2:21;
then consider x being Element of S such that
A7: ( x in D & (LowerAdj g) . t <= x ) by A2, A5, WAYBEL_3:def 1;
g . x in g .: D by A7, FUNCT_2:43;
then ( t <= g . x & g . x <= sup (g .: D) ) by A6, A7, WAYBEL_1:9, YELLOW_2:24;
hence t <= sup (g .: D) by ORDERS_2:26; :: thesis: verum

end;

then g . (sup D) <= sup (g .: D) by A4, YELLOW_0:32;
hence "\/" (g .: D),T = g . ("\/" D,S) by A3, ORDERS_2:25; :: thesis: verum