theorem ISum: :: LATTAD_1:18

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