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

now :: thesis: for a, b, c being Element of L holds 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)))

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
.= ((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:12; :: thesis: verum