let S, T be with_infima Poset; :: thesis: 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; :: thesis: 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; :: thesis: ( 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;

hereby :: thesis: ( f . (x "/\" y) = (f . x) "/\" (f . y) implies f preserves_inf_of {x,y} )

A2: ex_inf_of {x,y},S by YELLOW_0:21;
assume A3: f preserves_inf_of {x,y} ; :: thesis: f . (x "/\" y) = (f . x) "/\" (f . y)
thus f . (x "/\" y) = f . (inf {x,y}) by YELLOW_0:40
.= inf (f .: {x,y}) by A3, A2
.= inf {(f . x),(f . y)} by A1, FUNCT_1:60
.= (f . x) "/\" (f . y) by YELLOW_0:40 ; :: thesis: verum

end;

assume A4: f . (x "/\" y) = (f . x) "/\" (f . y) ; :: thesis: f preserves_inf_of {x,y}
assume ex_inf_of {x,y},S ; :: according to WAYBEL_0:def 30 :: thesis: ( 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; :: thesis: "/\" ((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 ; :: thesis: verum