theorem ThA5: :: LATTAD_1:21

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