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 Th29;
LowerAdj (corestr k) is waybelow-preserving
proof
let t, t9 be Element of (Image k); :: according to WAYBEL34:def 8 :: thesis: ( t << t9 implies (LowerAdj (corestr k)) . t << (LowerAdj (corestr k)) . t9 )
A4: LowerAdj (corestr k) = inclusion k by Th29;
then A5: (LowerAdj (corestr k)) . t = t by FUNCT_1:18;
(LowerAdj (corestr k)) . t9 = t9 by A4, FUNCT_1:18;
hence ( t << t9 implies (LowerAdj (corestr k)) . t << (LowerAdj (corestr k)) . t9 ) by A2, A5; :: thesis: verum
end;
then corestr k is directed-sups-preserving by A1, A3, Th23;
hence k is directed-sups-preserving by Th30; :: thesis: verum