theorem Lem36X: :: LATTAD_1:30

for L being GAD_Lattice
for x, y being Element of L holds x "\/" (x "\/" y) = x "\/" y