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

now :: thesis: for a, b, c being Element of L holds the L_meet of L . (a,( the L_join of L . (b,c))) = the L_join of L . (( the L_meet of L . (a,b)),( the L_meet of L . (a,c)))

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

end;

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