let L be complete LATTICE; :: thesis: for k being kernel Function of L,L holds
( k is directed-sups-preserving iff corestr k is directed-sups-preserving )
let k be kernel Function of L,L; :: thesis: ( k is directed-sups-preserving iff corestr k is directed-sups-preserving )
set ck = corestr k;
[(corestr k),(inclusion k)] is Galois by WAYBEL_1:39;
then A1: inclusion k is lower_adjoint ;
A2: k = (inclusion k) * (corestr k) by WAYBEL_1:32;

hereby :: thesis: ( corestr k is directed-sups-preserving implies k is directed-sups-preserving )

assume A3: k is directed-sups-preserving ; :: thesis: corestr k is directed-sups-preserving
thus corestr k is directed-sups-preserving :: thesis: verum

proof

let D be Subset of L; :: according to WAYBEL_0:def 37 :: thesis: ( D is empty or not D is directed or corestr k preserves_sup_of D )
assume ( not D is empty & D is directed ) ; :: thesis: corestr k preserves_sup_of D
then A4: k preserves_sup_of D by A3;
assume ex_sup_of D,L ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (corestr k) .: D, Image k & "\/" (((corestr k) .: D),(Image k)) = (corestr k) . ("\/" (D,L)) )
then A5: sup (k .: D) = k . (sup D) by A4
.= (inclusion k) . ((corestr k) . (sup D)) by A2, FUNCT_2:15
.= (corestr k) . (sup D) by FUNCT_1:18 ;
thus ex_sup_of (corestr k) .: D, Image k by YELLOW_0:17; :: thesis: "\/" (((corestr k) .: D),(Image k)) = (corestr k) . ("\/" (D,L))
A6: ex_sup_of (inclusion k) .: ((corestr k) .: D),L by YELLOW_0:17;
A7: Image k is sups-inheriting by WAYBEL_1:53;
ex_sup_of (corestr k) .: D,L by YELLOW_0:17;
then A8: "\/" (((corestr k) .: D),L) in the carrier of (Image k) by A7;
(corestr k) .: D = (inclusion k) .: ((corestr k) .: D) by WAYBEL15:12;
hence sup ((corestr k) .: D) = sup ((inclusion k) .: ((corestr k) .: D)) by A6, A8, YELLOW_0:64
.= (corestr k) . (sup D) by A2, A5, RELAT_1:126 ;
:: thesis: verum

end;

end;

thus ( corestr k is directed-sups-preserving implies k is directed-sups-preserving ) by A1, A2, WAYBEL15:11; :: thesis: verum