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

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