let S, T be complete LATTICE; :: thesis: for g being infs-preserving Function of S,T st g is one-to-one holds
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
let g be infs-preserving Function of S,T; :: thesis: ( g is one-to-one implies for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open ) )
assume A1: g is one-to-one ; :: thesis: for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
let X be Scott TopAugmentation of T; :: thesis: for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
let Y be Scott TopAugmentation of S; :: thesis: for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
[g,(LowerAdj g)] is Galois by Def1;
then LowerAdj g is onto by A1, WAYBEL_1:27;
then A2: rng (LowerAdj g) = the carrier of S by FUNCT_2:def 3;
A3: RelStr(# the carrier of Y, the InternalRel of Y #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;
A4: RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;
A5: [#] Y = the carrier of Y ;
let d be Function of X,Y; :: thesis: ( d = LowerAdj g implies ( g is directed-sups-preserving iff d is open ) )
assume A6: d = LowerAdj g ; :: thesis: ( g is directed-sups-preserving iff d is open )
A7: Y | (rng d) = TopStruct(# the carrier of Y, the topology of Y #) by A2, A3, A5, A6, TSEP_1:93;
thus ( g is directed-sups-preserving implies d is open ) :: thesis: ( d is open implies g is directed-sups-preserving )

proof

assume g is directed-sups-preserving ; :: thesis: d is open
then for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y by Th21;
then A8: d is relatively_open by A6, Th26;
let V be Subset of X; :: according to T_0TOPSP:def 2 :: thesis: ( not V is open or d .: V is open )
assume V is open ; :: thesis: d .: V is open
then d .: V is open Subset of (Y | (rng d)) by A8;
hence d .: V in the topology of Y by A7, PRE_TOPC:def 2; :: according to PRE_TOPC:def 2 :: thesis: verum

end;

assume A9: for V being Subset of X st V is open holds
d .: V is open ; :: according to T_0TOPSP:def 2 :: thesis: g is directed-sups-preserving

now :: thesis: for X9 being Scott TopAugmentation of T
for Y9 being Scott TopAugmentation of S
for V9 being open Subset of X9 holds uparrow ((LowerAdj g) .: V9) is open Subset of Y9

let X9 be Scott TopAugmentation of T; :: thesis: for Y9 being Scott TopAugmentation of S
for V9 being open Subset of X9 holds uparrow ((LowerAdj g) .: V9) is open Subset of Y9
let Y9 be Scott TopAugmentation of S; :: thesis: for V9 being open Subset of X9 holds uparrow ((LowerAdj g) .: V9) is open Subset of Y9
let V9 be open Subset of X9; :: thesis: uparrow ((LowerAdj g) .: V9) is open Subset of Y9
A10: RelStr(# the carrier of X9, the InternalRel of X9 #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;
A11: RelStr(# the carrier of Y9, the InternalRel of Y9 #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;
reconsider V = V9 as Subset of X by A4, A10;
reconsider V = V as open Subset of X by A4, A10, YELLOW_9:50;
reconsider d9 = d as Function of X9,Y9 by A3, A4, A10, A11;
d .: V is open by A9;
then A12: d9 .: V9 is open Subset of Y9 by A3, A11, YELLOW_9:50;
then d9 .: V9 is upper by WAYBEL11:def 4;
then A13: uparrow (d9 .: V9) c= d9 .: V9 by WAYBEL_0:24;
d9 .: V9 c= uparrow (d9 .: V9) by WAYBEL_0:16;
then uparrow (d9 .: V9) = d9 .: V9 by A13;
hence uparrow ((LowerAdj g) .: V9) is open Subset of Y9 by A6, A11, A12, WAYBEL_0:13; :: thesis: verum

end;

hence g is directed-sups-preserving by Th21; :: thesis: verum