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

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 & RelStr(# the carrier of Y,the InternalRel of Y #) = RelStr(# the carrier of L,the InternalRel of L #) ) 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, Th34;
(inclusion k) .: B = V by WAYBEL15:14;
hence uparrow V is open Subset of Y by A2, A3, A6, Th23; :: 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

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 & RelStr(# the carrier of Y,the InternalRel of Y #) = RelStr(# the carrier of L,the InternalRel of L #) ) 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:14; :: thesis: verum

end;

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