for S, T being complete LATTICE
for g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for Z being Scott TopAugmentation of Image (LowerAdj g)
for d being Function of X,Y
for d9 being Function of X,Z st d = LowerAdj g & d9 = d & d is relatively_open holds
d9 is open