let L be Lattice; :: thesis: the L_join of L is_distributive_wrt the L_join of L

now

let a, b, c be Element of L; :: thesis: the L_join of L . a,(the L_join of L . b,c) = the L_join of L . (the L_join of L . a,b),(the L_join of L . a,c)
thus the L_join of L . a,(the L_join of L . b,c) = a "\/" (b "\/" c)
.= (a "\/" b) "\/" c by LATTICES:def 5
.= ((a "\/" a) "\/" b) "\/" c by LATTICES:17
.= ((a "\/" b) "\/" a) "\/" c by LATTICES:def 5
.= (a "\/" b) "\/" (a "\/" c) by LATTICES:def 5
.= the L_join of L . (the L_join of L . a,b),(the L_join of L . a,c) ; :: thesis: verum

end;

hence the L_join of L is_distributive_wrt the L_join of L by BINOP_1:24; :: thesis: verum