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, t' be Element of T; :: according to WAYBEL34:def 8 :: thesis: ( t << t' implies (LowerAdj g) . t << (LowerAdj g) . t' )
assume A3: t << t' ; :: thesis: (LowerAdj g) . t << (LowerAdj g) . t'
let D be non empty directed Subset of S; :: according to WAYBEL_3:def 1 :: thesis: ( not (LowerAdj g) . t' <= "\/" D,S or ex b₁ being Element of the carrier of S st
( b₁ in D & (LowerAdj g) . t <= b₁ ) )
assume (LowerAdj g) . t' <= sup D ; :: thesis: ex b₁ being Element of the carrier of S st
( b₁ in D & (LowerAdj g) . t <= b₁ )
then A4: t' <= g . (sup D) by A2, WAYBEL_1:9;
( g preserves_sup_of D & ex_sup_of D,S ) by A1, WAYBEL_0:def 37, YELLOW_0:17;
then ( g . (sup D) = sup (g .: D) & g .: D is directed & not g .: D is empty ) by WAYBEL_0:def 31, YELLOW_2:17;
then consider x being Element of T such that
A5: ( x in g .: D & t <= x ) by A3, A4, WAYBEL_3:def 1;
consider s being set such that
A6: ( s in the carrier of S & s in D & x = g . s ) by A5, FUNCT_2:115;
reconsider s = s as Element of S by A6;
take s ; :: thesis: ( s in D & (LowerAdj g) . t <= s )
thus ( s in D & (LowerAdj g) . t <= s ) by A2, A5, A6, WAYBEL_1:9; :: thesis: verum