let L be with_infima Poset; :: thesis: for f being Function of L,L st f is filtered-infs-preserving holds
f is monotone
let f be Function of L,L; :: thesis: ( f is filtered-infs-preserving implies f is monotone )
assume A1: f is filtered-infs-preserving ; :: thesis: f is monotone
let x, y be Element of L; :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of L holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ ) )
assume A2: x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of L holds
( not b₁ = f . x or not b₂ = f . y or b₁ <= b₂ )
let a, b be Element of L; :: thesis: ( not a = f . x or not b = f . y or a <= b )
assume A3: ( a = f . x & b = f . y ) ; :: thesis: a <= b
A4: x = x "/\" y by A2, YELLOW_0:25;
( x <= x & x <= y ) by A2;
then A5: x is_<=_than {x,y} by YELLOW_0:8;
for c being Element of L st c is_<=_than {x,y} holds
c <= x by YELLOW_0:8;
then A6: ex_inf_of {x,y},L by A5, YELLOW_0:31;
for c, d being Element of L st c in {x,y} & d in {x,y} holds
ex z being Element of L st
( z in {x,y} & z <= c & z <= d )

proof

let c, d be Element of L; :: thesis: ( c in {x,y} & d in {x,y} implies ex z being Element of L st
( z in {x,y} & z <= c & z <= d ) )
assume A7: ( c in {x,y} & d in {x,y} ) ; :: thesis: ex z being Element of L st
( z in {x,y} & z <= c & z <= d )
take x ; :: thesis: ( x in {x,y} & x <= c & x <= d )
thus x in {x,y} by TARSKI:def 2; :: thesis: ( x <= c & x <= d )
thus ( x <= c & x <= d ) by A2, A7, TARSKI:def 2; :: thesis: verum

end;

then ( {x,y} is filtered & not {x,y} is empty ) by WAYBEL_0:def 2;
then f preserves_inf_of {x,y} by A1, WAYBEL_0:def 36;
then A8: inf (f .: {x,y}) = f . (inf {x,y}) by A6, WAYBEL_0:def 30
.= f . x by A4, YELLOW_0:40 ;
dom f = the carrier of L by FUNCT_2:def 1;
then f . x = inf {(f . x),(f . y)} by A8, FUNCT_1:118
.= (f . x) "/\" (f . y) by YELLOW_0:40 ;
hence a <= b by A3, YELLOW_0:23; :: thesis: verum