theorem IMeet: :: LATTAD_1:19

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