theorem LatWal2: :: LATWAL_2:12

for W being WA-Lattice
for a, b being Element of W holds a <= a "\/" b by YELLOW_0:22;