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 D9 = 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 .: D9 by A1, YELLOW_2:13;

hence f . ("/\" (D,S)) <= inf (f .: D) by YELLOW_0:33; :: thesis: verum

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 D9 = 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 .: D9 by A1, YELLOW_2:13;

hence f . ("/\" (D,S)) <= inf (f .: D) by YELLOW_0:33; :: thesis: verum