let a be Element of L; :: thesis: R29(L,a,a)
a "\/" a = a by ROBBINS1:def 7;
hence R29(L,a,a) by LATTICES:def 3; :: thesis: verum