theorem Th14: :: WAYBEL17:14

for S being lower-bounded up-complete LATTICE
for T being lower-bounded continuous LATTICE
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )