theorem Th12: :: WAYBEL17:12

for S, T being lower-bounded continuous LATTICE
for f being Function of S,T st f is directed-sups-preserving holds
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)