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