let L be Lattice; the L_meet of L is_distributive_wrt the L_meet of L
now let a,
b,
c be
Element of
L;
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
by LATTICES:18
.=
((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)
;
verum end;
hence
the L_meet of L is_distributive_wrt the L_meet of L
by BINOP_1:24; verum