:: deftheorem defines satisfying_WA LATWAL_1:def 5 :
for L being non empty LattStr holds
( L is satisfying_WA iff for x, y, z being Element of L holds x "/\" (y "\/" (x "\/" z)) = x );