let a, b be Element of L; :: according to BINOP_1:def 13 :: thesis: the L_join of L . a,b = the L_join of L . b,a
thus the L_join of L . a,b = b "\/" a by LATTICES:def 1
.= the L_join of L . b,a ; :: thesis: verum