let S be Semilattice; :: thesis: for x being Element of S holds x "/\" is monotone
let x be Element of S; :: thesis: x "/\" is monotone
let s1, s2 be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( s1 <= s2 implies (x "/\") . s1 <= (x "/\") . s2 )
assume A1: s1 <= s2 ; :: thesis: (x "/\") . s1 <= (x "/\") . s2
A2: ex_inf_of {x,s1},S by YELLOW_0:21;
then A3: x "/\" s1 <= x by YELLOW_0:19;
x "/\" s1 <= s1 by A2, YELLOW_0:19;
then ( ex_inf_of {x,s2},S & x "/\" s1 <= s2 ) by A1, ORDERS_2:3, YELLOW_0:21;
then x "/\" s1 <= x "/\" s2 by A3, YELLOW_0:19;
then (x "/\") . s1 <= x "/\" s2 by Def18;
hence (x "/\") . s1 <= (x "/\") . s2 by Def18; :: thesis: verum