let f be Function of L1,L2; :: thesis: ( f is infs-preserving implies ( f is filtered-infs-preserving & f is meet-preserving ) )
assume A1: for X being Subset of L1 holds f preserves_inf_of X ; :: according to WAYBEL_0:def 32 :: thesis: ( f is filtered-infs-preserving & f is meet-preserving )
hence for X being Subset of L1 st not X is empty & X is filtered holds
f preserves_inf_of X ; :: according to WAYBEL_0:def 36 :: thesis: f is meet-preserving
thus for x, y being Element of L1 holds f preserves_inf_of {x,y} by A1; :: according to WAYBEL_0:def 34 :: thesis: verum