theorem LemmaSum: :: LATWAL_1:9

for L being WA_Lattice
for x, y being Element of L holds x [= x "\/" y