theorem :: LATWAL_1:5

for L being WA_Lattice
for x, y being Element of L holds
( x "\/" y = y iff x [= y ) by LATTICES:def 3;