:: deftheorem DefW33 defines satisfying_W3' LATWAL_1:def 2 :
for L being non empty LattStr holds
( L is satisfying_W3' iff for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 );