theorem Idem: :: LATTAD_1:24

for L being GAD_Lattice
for x being Element of L holds x [= x