theorem Th25: :: WAYBEL34:25

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 V being open Subset of X holds (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))