Let q1 and q2 be given.
Assume Hq1Q: q1 ∈ rational_numbers.
Assume Hq2Q: q2 ∈ rational_numbers.
We prove the intermediate claim Hq2fam: open_interval q1 q2 ∈ {open_interval q1 q2'|q2' ∈ rational_numbers}.
An exact proof term for the current goal is (ReplI rational_numbers (λq2' : set ⇒ open_interval q1 q2') q2 Hq2Q).
An exact proof term for the current goal is (famunionI rational_numbers (λq1' : set ⇒ {open_interval q1' q2'|q2' ∈ rational_numbers}) q1 (open_interval q1 q2) Hq1Q Hq2fam).
∎