let S, T be complete LATTICE; :: thesis: for g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S st ( for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ) holds
for d being Function of X,Y st d = LowerAdj g holds
d is relatively_open
let g be infs-preserving Function of S,T; :: thesis: for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S st ( for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ) holds
for d being Function of X,Y st d = LowerAdj g holds
d is relatively_open
let X be Scott TopAugmentation of T; :: thesis: for Y being Scott TopAugmentation of S st ( for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ) holds
for d being Function of X,Y st d = LowerAdj g holds
d is relatively_open
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 ) implies for d being Function of X,Y st d = LowerAdj g holds
d is relatively_open )
assume A1: for V being open Subset of X holds uparrow ((LowerAdj g) .: V) is open Subset of Y ; :: thesis: for d being Function of X,Y st d = LowerAdj g holds
d is relatively_open
let d be Function of X,Y; :: thesis: ( d = LowerAdj g implies d is relatively_open )
assume A2: d = LowerAdj g ; :: thesis: d is relatively_open
let V be open Subset of X; :: according to WAYBEL34:def 9 :: thesis: d .: V is open Subset of (Y | (rng d))
reconsider A = uparrow ((LowerAdj g) .: V) as open Subset of Y by A1;
d .: V = A /\ (rng d) by A2, Th27;
then A3: ( d .: V = ([#] (Y | (rng d))) /\ A & A in the topology of Y ) by PRE_TOPC:def 5, PRE_TOPC:def 10;
then reconsider B = d .: V as Subset of (Y | (rng d)) by XBOOLE_1:17;
B in the topology of (Y | (rng d)) by A3, PRE_TOPC:def 9;
hence d .: V is open Subset of (Y | (rng d)) by PRE_TOPC:def 5; :: thesis: verum