:: deftheorem defines satisfying_4_McKenzie_axioms ROBBINS5:def 6 :
for L being non empty LattStr holds
( L is satisfying_4_McKenzie_axioms iff ( L is satisfying_McKenzie_1 & L is satisfying_McKenzie_2 & L is satisfying_McKenzie_3 & L is satisfying_McKenzie_4 ) );