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:29;
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:100;
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 Th23;
then A8: d is relatively_open by A6, Th28;
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, Def9;
hence d .: V in the topology of Y by A7, PRE_TOPC:def 5; :: according to PRE_TOPC:def 5 :: 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

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

end;

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