let L be Lattice; the L_join of L is_distributive_wrt the L_join of L
now for a, b, c being Element of L holds the L_join of L . (a,( the L_join of L . (b,c))) = the L_join of L . (( the L_join of L . (a,b)),( the L_join of L . (a,c)))let a,
b,
c be
Element of
L;
the L_join of L . (a,( the L_join of L . (b,c))) = the L_join 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_join of L . (b,c))) =
a "\/" (b "\/" c)
.=
(a "\/" b) "\/" c
by LATTICES:def 5
.=
((a "\/" a) "\/" b) "\/" c
.=
((a "\/" b) "\/" a) "\/" c
by LATTICES:def 5
.=
(a "\/" b) "\/" (a "\/" c)
by LATTICES:def 5
.=
the
L_join 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_join of L
by BINOP_1:12; verum