:: deftheorem defW3 defines satisfying_W3 LATWAL_1:def 3 :
for L being non empty meet-commutative meet-absorbing join-absorbing LattStr holds
( L is satisfying_W3 iff for v2, v1, v0 being Element of L holds v1 [= (v0 "\/" v1) "/\" (v2 "\/" v1) );