let a be Element of L; :: according to BINOP_1:def 4 :: thesis: the L_join of L . (a,a) = a
thus the L_join of L . (a,a) = a "\/" a
.= a ; :: thesis: verum