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