let a, b, c be Element of L; BINOP_1:def 3 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)),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
.=
the L_meet of L . (( the L_meet of L . (a,b)),c)
; verum