set b = the Element of L2;

defpred S_{1}[ set , set ] means for a1 being Element of L1 st L1 = a1 holds

L2 = the Element of L2;

A2: for x being Element of L1 holds S_{1}[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

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

defpred S

L2 = the Element of L2;

A1: now :: thesis: for x being Element of L1 ex b being Element of L2 st S_{1}[x,b]

consider f being Function of L1,L2 such that let x be Element of L1; :: thesis: ex b being Element of L2 st S_{1}[x,b]

take b = the Element of L2; :: thesis: S_{1}[x,b]

thus S_{1}[x,b]
; :: thesis: verum

end;take b = the Element of L2; :: thesis: S

thus S

A2: for x being Element of L1 holds S

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 2 :: thesis: f . (a1 "/\" b1) = (f . a1) "/\" (f . b1)
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;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

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