theorem :: LATTAD_1:61

for L being with_zero GAD_Lattice
for x being Element of L holds (bottom L) "\/" x = x