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