set b = the Element of L2;
defpred S₁[ set , set ] means for a1 being Element of L1 st L1 = a1 holds
L2 = the Element of L2;

A1: now :: thesis: for x being Element of L1 ex b being Element of L2 st S₁[x,b]

let x be Element of L1; :: thesis: ex b being Element of L2 st S₁[x,b]
take b = the Element of L2; :: thesis: S₁[x,b]
thus S₁[x,b] ; :: thesis: verum

end;

consider f being Function of L1,L2 such that
A2: for x being Element of L1 holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: ( f is "\/"-preserving & f is "/\"-preserving )
thus f is "\/"-preserving :: thesis: f is "/\"-preserving

proof

let a1, b1 be Element of L1; :: according to LATTICE4:def 1 :: thesis: f . (a1 "\/" b1) = (f . a1) "\/" (f . b1)
thus f . (a1 "\/" b1) = the Element of L2 by A2
.= the Element of L2 "\/" the Element of L2
.= (f . a1) "\/" the Element of L2 by A2
.= (f . a1) "\/" (f . b1) by A2 ; :: thesis: verum

end;

let a1, b1 be Element of L1; :: according to LATTICE4:def 2 :: thesis: f . (a1 "/\" b1) = (f . a1) "/\" (f . b1)
thus f . (a1 "/\" b1) = the Element of L2 by A2
.= the Element of L2 "/\" the Element of L2
.= (f . a1) "/\" the Element of L2 by A2
.= (f . a1) "/\" (f . b1) by A2 ; :: thesis: verum