We will prove basis_on R (order_topology_basis R).
Set T to be the term order_topology R.
We prove the intermediate claim HT: topology_on R T.
An exact proof term for the current goal is order_topology_R_is_topology.
We prove the intermediate claim HCsub: ∀c ∈ order_topology_basis R, c ∈ T.
Let c be given.
Assume HcB: c ∈ order_topology_basis R.
We will prove c ∈ T.
Set A to be the term {I ∈ 𝒫 R|∃a1 ∈ R, ∃b1 ∈ R, I = {x ∈ R|order_rel R a1 x ∧ order_rel R x b1}}.
Set B to be the term {I ∈ 𝒫 R|∃b1 ∈ R, I = {x ∈ R|order_rel R x b1}}.
Set C to be the term {I ∈ 𝒫 R|∃a1 ∈ R, I = {x ∈ R|order_rel R a1 x}}.
We prove the intermediate claim HcPow: c ∈ 𝒫 R.
Set Bold to be the term (A ∪ B ∪ C).
Apply (binunionE' Bold {R} c (c ∈ 𝒫 R)) to the current goal.
Assume HcU: c ∈ Bold.
Apply (binunionE' (A ∪ B) C c (c ∈ 𝒫 R)) to the current goal.
Assume HcAB: c ∈ (A ∪ B).
Apply (binunionE' A B c (c ∈ 𝒫 R)) to the current goal.
Assume HcA: c ∈ A.
An exact proof term for the current goal is (SepE1 (𝒫 R) (λI0 : set ⇒ ∃a0 ∈ R, ∃b0 ∈ R, I0 = {x ∈ R|order_rel R a0 x ∧ order_rel R x b0}) c HcA).
Assume HcB0: c ∈ B.
An exact proof term for the current goal is (SepE1 (𝒫 R) (λI0 : set ⇒ ∃b0 ∈ R, I0 = {x ∈ R|order_rel R x b0}) c HcB0).
An exact proof term for the current goal is HcAB.
Assume HcC: c ∈ C.
An exact proof term for the current goal is (SepE1 (𝒫 R) (λI0 : set ⇒ ∃a0 ∈ R, I0 = {x ∈ R|order_rel R a0 x}) c HcC).
An exact proof term for the current goal is HcU.
Assume HcR: c ∈ {R}.
We prove the intermediate claim HcEq: c = R.
An exact proof term for the current goal is (SingE R c HcR).
rewrite the current goal using HcEq (from left to right).
An exact proof term for the current goal is (Self_In_Power R).
An exact proof term for the current goal is HcB.
An exact proof term for the current goal is (generated_topology_contains_elem R (order_topology_basis R) c HcPow HcB).
We prove the intermediate claim Href: ∀U ∈ T, ∀x ∈ U, ∃c ∈ order_topology_basis R, x ∈ c ∧ c ⊆ U.
Let U be given.
Assume HU: U ∈ T.
Let x be given.
Assume HxU: x ∈ U.
We will prove ∃c ∈ order_topology_basis R, x ∈ c ∧ c ⊆ U.
We prove the intermediate claim HTdef: T = generated_topology R (order_topology_basis R).
Use reflexivity.
We prove the intermediate claim HUgen: U ∈ generated_topology R (order_topology_basis R).
rewrite the current goal using HTdef (from right to left).
An exact proof term for the current goal is HU.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ order_topology_basis R, x0 ∈ b ∧ b ⊆ U0) U HUgen x HxU).
An exact proof term for the current goal is (andEL (basis_on R (order_topology_basis R)) (generated_topology R (order_topology_basis R) = T) (lemma13_2_basis_from_open_subcollection R T (order_topology_basis R) HT HCsub Href)).
∎