Let b be given.

Assume Hb: b ∈ rational_open_intervals_basis.

Apply (famunionE_impred rational_numbers (λq1 : set ⇒ {open_interval q1 q2|q2 ∈ rational_numbers}) b Hb (∃q1, ∃q2, (q1 ∈ rational_numbers ∧ q2 ∈ rational_numbers ∧ b = open_interval q1 q2))) to the current goal.

Let q1 be given.

Assume Hq1Q: q1 ∈ rational_numbers.

Assume Hbq1: b ∈ {open_interval q1 q2|q2 ∈ rational_numbers}.

Apply (ReplE_impred rational_numbers (λq2 : set ⇒ open_interval q1 q2) b Hbq1 (∃q1, ∃q2, (q1 ∈ rational_numbers ∧ q2 ∈ rational_numbers ∧ b = open_interval q1 q2))) to the current goal.

Let q2 be given.

Assume Hq2Q: q2 ∈ rational_numbers.

Assume Heq: b = open_interval q1 q2.

We use q1 to witness the existential quantifier.

We use q2 to witness the existential quantifier.

Apply andI to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Hq1Q.

An exact proof term for the current goal is Hq2Q.

An exact proof term for the current goal is Heq.

∎