Let a be given.
Assume HaR.
We will prove {a} ∉ R_standard_topology.
Assume Hsing: {a} ∈ R_standard_topology.
We will prove False.
Set Bq to be the term rational_open_intervals_basis.
We prove the intermediate claim HBq: basis_on R Bq.
An exact proof term for the current goal is (andEL (basis_on R Bq) (generated_topology R Bq = R_standard_topology) ex13_8a_rational_intervals_basis_standard).
We prove the intermediate claim HeqStd: generated_topology R Bq = R_standard_topology.
An exact proof term for the current goal is (andER (basis_on R Bq) (generated_topology R Bq = R_standard_topology) ex13_8a_rational_intervals_basis_standard).
We prove the intermediate claim HsingGen: {a} ∈ generated_topology R Bq.
rewrite the current goal using HeqStd (from left to right).
An exact proof term for the current goal is Hsing.
We prove the intermediate claim HTgen: topology_on R (generated_topology R Bq).
An exact proof term for the current goal is (lemma_topology_from_basis R Bq HBq).
We prove the intermediate claim Hopen: open_in R (generated_topology R Bq) {a}.
An exact proof term for the current goal is (andI (topology_on R (generated_topology R Bq)) ({a} ∈ generated_topology R Bq) HTgen HsingGen).
We prove the intermediate claim HexFam: ∃Fam ∈ 𝒫 Bq, ⋃ Fam = {a}.
An exact proof term for the current goal is (open_sets_as_unions_of_basis R Bq HBq {a} Hopen).
Apply HexFam to the current goal.
Let Fam be given.
Assume HFcore.
Apply HFcore to the current goal.
Assume HFamPow: Fam ∈ 𝒫 Bq.
Assume HUnionEq: ⋃ Fam = {a}.
We prove the intermediate claim HaUnion: a ∈ ⋃ Fam.
rewrite the current goal using HUnionEq (from left to right).
An exact proof term for the current goal is (SingI a).
Apply (UnionE_impred Fam a HaUnion False) to the current goal.
Let I be given.
Assume HaI HIinFam.
We prove the intermediate claim HIbq: I ∈ Bq.
An exact proof term for the current goal is (PowerE Bq Fam HFamPow I HIinFam).
Apply (famunionE_impred rational_numbers (λq1 : set ⇒ {open_interval q1 q2|q2 ∈ rational_numbers}) I HIbq False) to the current goal.
Let q1 be given.
Assume Hq1Q HIq1.
Apply (ReplE_impred rational_numbers (λq2 : set ⇒ open_interval q1 q2) I HIq1 False) to the current goal.
Let q2 be given.
Assume Hq2Q HIeq.
We prove the intermediate claim HaInt: a ∈ open_interval q1 q2.
rewrite the current goal using HIeq (from right to left).
An exact proof term for the current goal is HaI.
We prove the intermediate claim Hq1a: Rlt q1 a.
An exact proof term for the current goal is (andEL (Rlt q1 a) (Rlt a q2) (SepE2 R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) a HaInt)).
We prove the intermediate claim Haq2: Rlt a q2.
An exact proof term for the current goal is (andER (Rlt q1 a) (Rlt a q2) (SepE2 R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) a HaInt)).
We prove the intermediate claim Hq1R: q1 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q1 Hq1Q).
We prove the intermediate claim Hq2R: q2 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q2 Hq2Q).
We prove the intermediate claim Hexq: ∃q ∈ rational_numbers, Rlt q1 q ∧ Rlt q a.
An exact proof term for the current goal is (rational_dense_between_reals q1 a Hq1R HaR Hq1a).
Apply Hexq to the current goal.
Let q be given.
Assume Hqcore.
Apply Hqcore to the current goal.
Assume HqQ Hqineq.
We prove the intermediate claim Hq1q: Rlt q1 q.
An exact proof term for the current goal is (andEL (Rlt q1 q) (Rlt q a) Hqineq).
We prove the intermediate claim Hqqa: Rlt q a.
An exact proof term for the current goal is (andER (Rlt q1 q) (Rlt q a) Hqineq).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim Hqq2: Rlt q q2.
An exact proof term for the current goal is (Rlt_tra q a q2 Hqqa Haq2).
We prove the intermediate claim HqInt: q ∈ open_interval q1 q2.
An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) q HqR (andI (Rlt q1 q) (Rlt q q2) Hq1q Hqq2)).
We prove the intermediate claim HqI: q ∈ I.
rewrite the current goal using HIeq (from left to right).
An exact proof term for the current goal is HqInt.
We prove the intermediate claim HqUnion: q ∈ ⋃ Fam.
An exact proof term for the current goal is (UnionI Fam q I HqI HIinFam).
We prove the intermediate claim HqSing: q ∈ {a}.
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HqUnion.
We prove the intermediate claim Hqeq: q = a.
An exact proof term for the current goal is (SingE a q HqSing).
We prove the intermediate claim HltAA: Rlt a a.
rewrite the current goal using Hqeq (from right to left) at position 1.
An exact proof term for the current goal is Hqqa.
An exact proof term for the current goal is (not_Rlt_refl a HaR HltAA).
∎