theorem EReal.real_strictly_between_infinities (ξ : ℝ) : ⊥ < ↑ξ ∧ ↑ξ < ⊤

Every real number lies strictly between -∞ and +∞ in the extended real line.