theorem IMeet: :: LATTAD_1:4

for L being AD_Lattice
for x being Element of L holds x "/\" x = x