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 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:24; :: thesis: verum