let L be complete LATTICE; :: thesis: for k being kernel Function of L,L st Image k is continuous & ( for x, y being Element of L
for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b ) ) holds
k is directed-sups-preserving
let k be kernel Function of L,L; :: thesis: ( Image k is continuous & ( for x, y being Element of L
for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b ) ) implies k is directed-sups-preserving )
assume that
A1: Image k is continuous and
A2: for x, y being Element of L
for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b ) ; :: thesis: k is directed-sups-preserving
set g = corestr k;
A3: corestr k is infs-preserving by Th33;
LowerAdj (corestr k) is waybelow-preserving

proof

let t, t' be Element of (Image k); :: according to WAYBEL34:def 8 :: thesis: ( t << t' implies (LowerAdj (corestr k)) . t << (LowerAdj (corestr k)) . t' )
LowerAdj (corestr k) = inclusion k by Th33;
then ( (LowerAdj (corestr k)) . t = t & (LowerAdj (corestr k)) . t' = t' ) by TMAP_1:91;
hence ( t << t' implies (LowerAdj (corestr k)) . t << (LowerAdj (corestr k)) . t' ) by A2; :: thesis: verum

end;

then corestr k is directed-sups-preserving by A1, A3, Th25;
hence k is directed-sups-preserving by Th34; :: thesis: verum