theorem Th25: :: WAYBEL17:25

for S being LATTICE
for T being complete 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 & w is compact ) } ,T) ) holds
f is monotone