let a be Element of L; :: thesis: (L,a,a)
thus a "\/" a = a ; :: according to LATTICES:def 3 :: thesis: verum