let L1, L2 be non empty RelStr ; :: thesis: for f being Function of L1,L2 st f is infs-preserving holds
f is meet-preserving
let f be Function of L1,L2; :: thesis: ( f is infs-preserving implies f is meet-preserving )
assume f is infs-preserving ; :: thesis: f is meet-preserving
then for x, y being Element of L1 holds f preserves_inf_of {x,y} by WAYBEL_0:def 32;
hence f is meet-preserving by WAYBEL_0:def 34; :: thesis: verum