 Least representatives of finite equivalence classes

On a finite linearly ordered structure with an equivalence relation, the formula $\forall y(y<x\to \neg E(y,x))$ selects exactly the least element of each equivalence class. Variable-recycling counting therefore expresses any prescribed lower bound on the number of classes. The order and equivalence-relation axioms use three variable names. Finiteness matters: densely interleaved infinite classes need not have least elements.