let L be complete LATTICE; :: thesis: for k being kernel Function of L,L holds
( k is directed-sups-preserving iff 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 )
let k be kernel Function of L,L; :: thesis: ( k is directed-sups-preserving iff 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 )
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: ( ( 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 ) implies k is directed-sups-preserving )

assume A4: k is directed-sups-preserving ; :: thesis: 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
let X be Scott TopAugmentation of Image k; :: thesis: 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
let Y be Scott TopAugmentation of L; :: thesis: for V being Subset of L st V is open Subset of X holds
uparrow V is open Subset of Y
A5: RelStr(# the carrier of X, the InternalRel of X #) = Image k by YELLOW_9:def 4;
let V be Subset of L; :: thesis: ( V is open Subset of X implies uparrow V is open Subset of Y )
assume V is open Subset of X ; :: thesis: uparrow V is open Subset of Y
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: verum

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: k is directed-sups-preserving

now :: thesis: for X being Scott TopAugmentation of Image k
for Y being Scott TopAugmentation of L
for V being open Subset of X holds uparrow ((LowerAdj (corestr k)) .: V) is open Subset of Y

set g = corestr k;
let X be Scott TopAugmentation of Image k; :: thesis: for Y being Scott TopAugmentation of L
for V being open Subset of X holds uparrow ((LowerAdj (corestr k)) .: V) is open Subset of Y
let Y be Scott TopAugmentation of L; :: thesis: for V being open Subset of X holds uparrow ((LowerAdj (corestr k)) .: V) is open Subset of Y
let V be open Subset of X; :: thesis: uparrow ((LowerAdj (corestr k)) .: V) is open Subset of Y
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: verum

end;

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