let S, T be complete LATTICE; :: thesis: for D being Subset of S
for f being Function of S,T st f is monotone holds
f . ("/\" D,S) <= inf (f .: D)
let D be Subset of S; :: thesis: for f being Function of S,T st f is monotone holds
f . ("/\" D,S) <= inf (f .: D)
let f be Function of S,T; :: thesis: ( f is monotone implies f . ("/\" D,S) <= inf (f .: D) )
reconsider D' = D as Subset of S ;
set infD = "/\" D,S;
assume A1: f is monotone ; :: thesis: f . ("/\" D,S) <= inf (f .: D)
"/\" D,S is_<=_than D by YELLOW_0:33;
then f . ("/\" D,S) is_<=_than f .: D' by A1, YELLOW_2:15;
hence f . ("/\" D,S) <= inf (f .: D) by YELLOW_0:33; :: thesis: verum