for S, T being with_suprema Poset
for f being Function of S,T
for x, y being Element of S holds
( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) )