let S, T be complete LATTICE; 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; 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; ( f is monotone implies f . ("/\" (D,S)) <= inf (f .: D) )
reconsider D9 = D as Subset of S ;
set infD = "/\" (D,S);
assume A1:
f is monotone
; f . ("/\" (D,S)) <= inf (f .: D)
"/\" (D,S) is_<=_than D
by YELLOW_0:33;
then
f . ("/\" (D,S)) is_<=_than f .: D9
by A1, YELLOW_2:13;
hence
f . ("/\" (D,S)) <= inf (f .: D)
by YELLOW_0:33; verum