let a, b be Element of L; :: according to BINOP_1:def 2 :: 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