theorem Lemat01: :: LATWAL_2:2

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