theorem LemmaX1: :: LATWAL_2:7

for W being WA-Lattice
for a, b being Element of W holds (a "/\" b) "\/" a = a by LATTICE3:17;