theorem interval_real_iff_two_points_and_between (I : Set ℝ) : (I.OrdConnected ∧ ∃ (a : ℝ) (c : ℝ), a ≠ c ∧ a ∈ I ∧ c ∈ I) ↔ (∃ (a : ℝ) (c : ℝ), a ≠ c ∧ a ∈ I ∧ c ∈ I) ∧ ∀ {a c b : ℝ}, a ∈ I → c ∈ I → a < b → b < c → b ∈ I

Proposition 1.4.1: A set I ⊆ ℝ is an interval if and only if it contains at least two points and, whenever a, c ∈ I and a < b < c, the point b also belongs to I.

theorem cantor_real_uncountable : Uncountable ℝ

Theorem 1.4.2 (Cantor): The set of real numbers ℝ is uncountable.