set b = the Element of L2;
defpred S1[ 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 S1[x,b]
let x be Element of L1; :: thesis: ex b being Element of L2 st S1[x,b]
take b = the Element of L2; :: thesis: S1[x,b]
thus S1[x,b] ; :: thesis: verum
end;
consider f being Function of L1,L2 such that
A2: for x being Element of L1 holds S1[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