let f be Function of S,T; :: thesis: ( f is meet-preserving implies f is monotone )
assume A1: f is meet-preserving ; :: thesis: f is monotone
let x, y be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or f . x <= f . y )
assume x <= y ; :: thesis: f . x <= f . y
then x = x "/\" y by YELLOW_0:25;
then f . x = (f . x) "/\" (f . y) by A1, WAYBEL_6:1;
hence f . x <= f . y by YELLOW_0:25; :: thesis: verum