theorem :: WAYBEL24:5

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