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