theorem ISum: :: LATTAD_1:3

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