theorem ThA4: :: LATTAD_1:20

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