let S, T be with_infima Poset; for f being Function of S,T
for x, y being Element of S holds
( f preserves_inf_of {x,y} iff f . (x "/\" y) = (f . x) "/\" (f . y) )
let f be Function of S,T; for x, y being Element of S holds
( f preserves_inf_of {x,y} iff f . (x "/\" y) = (f . x) "/\" (f . y) )
let x, y be Element of S; ( f preserves_inf_of {x,y} iff f . (x "/\" y) = (f . x) "/\" (f . y) )
A1:
dom f = the carrier of S
by FUNCT_2:def 1;
assume A4:
f . (x "/\" y) = (f . x) "/\" (f . y)
; f preserves_inf_of {x,y}
assume
ex_inf_of {x,y},S
; WAYBEL_0:def 30 ( ex_inf_of f .: {x,y},T & "/\" ((f .: {x,y}),T) = f . ("/\" ({x,y},S)) )
f .: {x,y} = {(f . x),(f . y)}
by A1, FUNCT_1:60;
hence
ex_inf_of f .: {x,y},T
by YELLOW_0:21; "/\" ((f .: {x,y}),T) = f . ("/\" ({x,y},S))
thus inf (f .: {x,y}) =
inf {(f . x),(f . y)}
by A1, FUNCT_1:60
.=
(f . x) "/\" (f . y)
by YELLOW_0:40
.=
f . (inf {x,y})
by A4, YELLOW_0:40
; verum