The fact that Fourier-Motzkin elimination gives a sound and complete procedure for determining whether a system of linear inequalities has a solution (and for computing the existential projection of the solution-set onto a subset of the variables). The proof is intuitive, very difficult to forget, and provides a useful procedure for hand-computations in low dimensions. Farkas' Lemma follows as an obvious consequence.

The general idea of variable elimination occurs throughout mathematics and logic and is closely connected to tools used to automate mathematics - for instance, the Resolution proof system is used in SAT-solving, for algebraic geometry we use Gröbner bases, for polynomial inequalities we use Cylindrical Algebraic Decomposition. Fourier-Motzkin elimination is a perfect introduction to the general technique and is often practically useful. Farkas' Lemma also motivates convex duality, a cornerstone of mathematical optimization.