theorem :: LATTICE8:4

for L1, L2 being lower-bounded LATTICE
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 ) ;