:: deftheorem defines satisfying_McKenzie_3 ROBBINS5:def 4 :
for L being non empty LattStr holds
( L is satisfying_McKenzie_3 iff for v2, v1, v0 being Element of L holds ((v0 "/\" v1) "\/" (v1 "/\" v2)) "\/" v1 = v1 );