let L be Lattice; ( L is D_Lattice implies the L_join of L is_distributive_wrt the L_meet of L )
assume A1:
L is D_Lattice
; the L_join of L is_distributive_wrt the L_meet of L
now let a,
b,
c be
Element of
L;
the L_join of L . a,(the L_meet of L . b,c) = the L_meet of L . (the L_join of L . a,b),(the L_join of L . a,c)thus the
L_join of
L . a,
(the L_meet of L . b,c) =
a "\/" (b "/\" c)
.=
(a "\/" b) "/\" (a "\/" c)
by A1, LATTICES:31
.=
the
L_meet of
L . (the L_join of L . a,b),
(the L_join of L . a,c)
;
verum end;
hence
the L_join of L is_distributive_wrt the L_meet of L
by BINOP_1:24; verum