for S, T being complete LATTICE
for f being monotone Function of S,T
for x being Element of S holds f . x = sup (f .: (downarrow x))