theorem Lemat0: :: LATWAL_2:1

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