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 Th29, Th30;
then A1: LowerAdj (corestr k) is waybelow-preserving by Th22;
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:53;
A3: inclusion k = LowerAdj (corestr k) by Th29;
then A4: (LowerAdj (corestr k)) . a = a by FUNCT_1:18;
(LowerAdj (corestr k)) . b = b by A3, FUNCT_1:18;
hence ( a = x & b = y implies ( x << y iff a << b ) ) by A1, A2, A4, Th32; :: thesis: verum