let a be Element of L; :: according to BINOP_1:def 15 :: thesis: the L_meet of L . (a,a) = a
thus the L_meet of L . (a,a) = a "/\" a
.= a by LATTICES:2 ; :: thesis: verum