let L be Lattice; :: thesis: the L_meet of L is_distributive_wrt the L_meet of L
now 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
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)
;
:: thesis: verum end;
hence
the L_meet of L is_distributive_wrt the L_meet of L
by BINOP_1:24; :: thesis: verum