let a, b, c be Element of L; :: according to BINOP_1:def 3 :: 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)),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) ; :: thesis: verum