let L be complete LATTICE; :: thesis:
let k be kernel Function of L,L; :: thesis:
A1: [(corestr k),(inclusion k)] is Galois by WAYBEL_1:39;
then A2: corestr k is upper_adjoint ;
then A3: inclusion k = LowerAdj (corestr k) by A1, Def1;

hereby :: thesis:

assume A4: k is directed-sups-preserving ; :: thesis:
let X be Scott TopAugmentation of Image k; :: thesis:
let Y be Scott TopAugmentation of L; :: thesis:
A5: RelStr(# the carrier of X, the InternalRel of X #) = Image k by YELLOW_9:def 4;
let V be Subset of L; :: thesis:
assume V is open Subset of X ; :: thesis:
then reconsider A = V as open Subset of X ;
reconsider B = A as Subset of (Image k) by A5;
A6: corestr k is directed-sups-preserving by A4, Th30;
(inclusion k) .: B = V by WAYBEL15:12;
hence uparrow V is open Subset of Y by A2, A3, A6, Th21; :: thesis:

end;

assume A7: for X being Scott TopAugmentation of Image k
for Y being Scott TopAugmentation of L
for V being Subset of L st V is open Subset of X holds
uparrow V is open Subset of Y ; :: thesis:

set g = corestr k;
let X be Scott TopAugmentation of Image k; :: thesis:
let Y be Scott TopAugmentation of L; :: thesis:
let V be open Subset of X; :: thesis:
RelStr(# the carrier of X, the InternalRel of X #) = Image k by YELLOW_9:def 4;
then reconsider B = V as Subset of (Image k) ;
the carrier of (Image k) c= the carrier of L by YELLOW_0:def 13;
then reconsider A = B as Subset of L by XBOOLE_1:1;
uparrow A is open Subset of Y by A7;
hence uparrow ((LowerAdj (corestr k)) .: V) is open Subset of Y by A3, WAYBEL15:12; :: thesis:

end;

then corestr k is directed-sups-preserving by A2, Th21;
hence k is directed-sups-preserving by Th30; :: thesis: