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