let L1, L2 be lower-bounded LATTICE; :: thesis: for f being Function of L1,L2 st f is infs-preserving & f is sups-preserving holds
( f is meet-preserving & f is join-preserving )
let f be Function of L1,L2; :: thesis: ( f is infs-preserving & f is sups-preserving implies ( f is meet-preserving & f is join-preserving ) )
assume A1: ( f is infs-preserving & f is sups-preserving ) ; :: thesis: ( f is meet-preserving & f is join-preserving )
thus f is meet-preserving :: thesis: f is join-preserving

proof

let x, y be Element of L1; :: according to WAYBEL_0:def 34 :: thesis: f preserves_inf_of {x,y}
thus f preserves_inf_of {x,y} by A1, WAYBEL_0:def 32; :: thesis: verum

end;

thus f is join-preserving :: thesis: verum

proof

let x, y be Element of L1; :: according to WAYBEL_0:def 35 :: thesis: f preserves_sup_of {x,y}
thus f preserves_sup_of {x,y} by A1, WAYBEL_0:def 33; :: thesis: verum

end;