theorem HyperplaneArrangement.wall_of_C_separates_distinct_chambers {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {arr : HyperplaneArrangement E} (C D : arr.Chamber) (hne : C.set ≠ D.set) (hlf : arr.IsLocallyFinite) : ∃ (η : AffineHyperplane E) (hη : η ∈ arr.hyperplanes), η.IsWall C.set ∧ SeparatesChambers η hη C D

Corollary of the wall-separation theorem: for distinct chambers $C, D$ in a locally finite arrangement, there exists a wall $η$ of $C$ that strictly separates $C$ from $D$. This is a cleaner repackaging of wall_separates_distinct_chambers with the inner membership discarded.