let L be non empty meet-associative /\-SemiLattStr ; :: thesis: the L_meet of L is associative
let a, b, c be Element of L; :: according to BINOP_1:def 14 :: 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