let a be Element of L; :: thesis: a [= a
thus a "\/" a = a by Th17; :: according to LATTICES:def 3 :: thesis: verum