let L be Lattice; :: thesis: ( L is D_Lattice implies the L_join of L is_distributive_wrt the L_meet of L )
assume A1: L is D_Lattice ; :: thesis: the L_join of L is_distributive_wrt the L_meet of L

now :: thesis: for a, b, c being Element of L holds the L_join of L . (a,( the L_meet of L . (b,c))) = the L_meet 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_meet of L . (b,c))) = the L_meet 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_meet of L . (b,c))) = a "\/" (b "/\" c)
.= (a "\/" b) "/\" (a "\/" c) by A1, LATTICES:11
.= the L_meet 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_meet of L by BINOP_1:12; :: thesis: verum