let L be complete LATTICE; :: thesis: for k being kernel Function of L,L st k is directed-sups-preserving holds
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 )
let k be kernel Function of L,L; :: thesis: ( k is directed-sups-preserving implies 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 ) )
set g = corestr k;
assume k is directed-sups-preserving ; :: thesis: 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 )
then ( corestr k is directed-sups-preserving & corestr k is infs-preserving ) by Th33, Th34;
then A1: LowerAdj (corestr k) is waybelow-preserving by Th24;
let x, y be Element of L; :: thesis: for a, b being Element of (Image k) st a = x & b = y holds
( x << y iff a << b )
let a, b be Element of (Image k); :: thesis: ( a = x & b = y implies ( x << y iff a << b ) )
A2: Image k is sups-inheriting by WAYBEL_1:56;
inclusion k = LowerAdj (corestr k) by Th33;
then ( (LowerAdj (corestr k)) . a = a & (LowerAdj (corestr k)) . b = b ) by TMAP_1:91;
hence ( a = x & b = y implies ( x << y iff a << b ) ) by A1, A2, Def8, Th36; :: thesis: verum