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