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:42;
then ( inclusion k is lower_adjoint & corestr k is upper_adjoint ) by WAYBEL_1:def 11, WAYBEL_1:def 12;
then A1: ( inclusion k is sups-preserving Function of (Image k),L & corestr k is infs-preserving ) ;
A2: ( k = (inclusion k) * (corestr k) & inclusion k = LowerAdj (corestr k) ) by Th33, WAYBEL_1:35;

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, WAYBEL_0:def 37;
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, WAYBEL_0:def 31
.= (inclusion k) . ((corestr k) . (sup D)) by A2, FUNCT_2:21
.= (corestr k) . (sup D) by TMAP_1:91 ;
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:56;
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, YELLOW_0:def 19;
(corestr k) .: D = (inclusion k) .: ((corestr k) .: D) by WAYBEL15:14;
hence sup ((corestr k) .: D) = sup ((inclusion k) .: ((corestr k) .: D)) by A6, A8, YELLOW_0:65
.= (corestr k) . (sup D) by A2, A5, RELAT_1:159 ;
:: thesis: verum

end;

end;

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