Let X, a and b be given.
Assume Hso: simply_ordered_set X.
Assume Ha: a ∈ X.
Assume Hb: b ∈ X.
Assume Hab: order_rel X a b.
Assume Hsucc: no_immediate_successor X a.
Assume Hpred: no_immediate_predecessor X b.
We will prove closure_of X (order_topology X) (order_interval X a b) = closed_interval_in X a b.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closure_of X (order_topology X) (order_interval X a b).
An exact proof term for the current goal is (ex17_5_closure_of_interval_in_order_topology X a b Hso Ha Hb x Hx).
Let x be given.
Assume Hx: x ∈ closed_interval_in X a b.
We will prove x ∈ closure_of X (order_topology X) (order_interval X a b).
Set Tx to be the term order_topology X.
Set I to be the term order_interval X a b.
Set B to be the term order_topology_basis X.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (order_topology_is_topology X Hso).
We prove the intermediate claim HI_subX: I ⊆ X.
An exact proof term for the current goal is (order_interval_subset X a b).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ (x0 = a ∨ order_rel X a x0) ∧ (x0 = b ∨ order_rel X x0 b)) x Hx).
We prove the intermediate claim Hdefcl: closure_of X (order_topology X) (order_interval X a b) = {x0 ∈ X|∀U : set, U ∈ Tx → x0 ∈ U → U ∩ I ≠ Empty}.
Use reflexivity.
rewrite the current goal using Hdefcl (from left to right).
Apply (SepI X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ I ≠ Empty) x HxX) to the current goal.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove U ∩ I ≠ Empty.
We prove the intermediate claim HUgen: U ∈ generated_topology X B.
An exact proof term for the current goal is HU.
We prove the intermediate claim Hexb: ∃b0 ∈ B, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (generated_topology_local_refine X B U x HUgen HxU).
Apply Hexb to the current goal.
Let b0 be given.
Assume Hb0core.
Apply Hb0core to the current goal.
Assume Hb0B Hb0pair.
We prove the intermediate claim Hxb0: x ∈ b0.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hb0subU: b0 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hexy: ∃y : set, y ∈ b0 ∧ y ∈ I.
An exact proof term for the current goal is (ex17_5_basis_elem_meets_interval X a b x b0 Hso Ha Hb Hab Hsucc Hpred Hx Hb0B Hxb0).
Apply Hexy to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume Hyb0 HyI.
Assume Hempty: U ∩ I = Empty.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (Hb0subU y Hyb0).
We prove the intermediate claim HyUI: y ∈ U ∩ I.
An exact proof term for the current goal is (binintersectI U I y HyU HyI).
We prove the intermediate claim HyE: y ∈ Empty.
rewrite the current goal using Hempty (from right to left).
An exact proof term for the current goal is HyUI.
An exact proof term for the current goal is (EmptyE y HyE).
∎