theorem CombinedMcKenzie: :: ROBBINS5:15

for L being non empty LattStr holds
( L is Lattice iff L is satisfying_4_McKenzie_axioms )