theorem Th1: :: WAYBEL_6:1

for S, T being Semilattice
for f being Function of S,T holds
( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) )