set z = the Element of L2;
reconsider f = the carrier of L1 --> the Element of L2 as Function of L1,L2 ;
take f ; :: thesis: ( f is meet-preserving & f is join-preserving )
for x, y being Element of L1 holds f . (x "/\" y) = (f . x) "/\" (f . y) by YELLOW_5:2;
hence f is meet-preserving by WAYBEL_6:1; :: thesis: f is join-preserving
for x, y being Element of L1 holds f . (x "\/" y) = (f . x) "\/" (f . y) by YELLOW_5:1;
hence f is join-preserving by WAYBEL_6:2; :: thesis: verum