Let X, a and b be given.
Assume Hso: simply_ordered_set X.
Assume HaX: a ∈ X.
Assume HbX: b ∈ X.
We will prove closure_of X (order_topology X) (order_interval X a b) ⊆ closed_interval_in X a b.
Set Tx to be the term order_topology X.
We prove the intermediate claim HTx: topology_on X Tx.
rewrite the current goal using (open_rays_subbasis_for_order_topology X Hso) (from right to left).
An exact proof term for the current goal is (topology_from_subbasis_is_topology X (open_rays_subbasis X) (open_rays_subbasis_is_subbasis X)).
We prove the intermediate claim Hsub: order_interval X a b ⊆ closed_interval_in X a b.
Let x be given.
Assume Hx: x ∈ order_interval X a b.
We will prove x ∈ closed_interval_in X a b.
We prove the intermediate claim Hxpack: x ∈ X ∧ (order_rel X a x ∧ order_rel X x b).
An exact proof term for the current goal is (order_intervalE X a b x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (order_rel X a x ∧ order_rel X x b) Hxpack).
We prove the intermediate claim Hrel: order_rel X a x ∧ order_rel X x b.
An exact proof term for the current goal is (andER (x ∈ X) (order_rel X a x ∧ order_rel X x b) Hxpack).
We prove the intermediate claim Hax: order_rel X a x.
An exact proof term for the current goal is (andEL (order_rel X a x) (order_rel X x b) Hrel).
We prove the intermediate claim Hxb: order_rel X x b.
An exact proof term for the current goal is (andER (order_rel X a x) (order_rel X x b) Hrel).
We prove the intermediate claim Hci_def: closed_interval_in X a b = {x0 ∈ X|(x0 = a ∨ order_rel X a x0) ∧ (x0 = b ∨ order_rel X x0 b)}.
Use reflexivity.
rewrite the current goal using Hci_def (from left to right).
Apply (SepI X (λx0 : set ⇒ (x0 = a ∨ order_rel X a x0) ∧ (x0 = b ∨ order_rel X x0 b)) x HxX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (orIR (x = a) (order_rel X a x) Hax).
An exact proof term for the current goal is (orIR (x = b) (order_rel X x b) Hxb).
We prove the intermediate claim Hclosed: closed_in X Tx (closed_interval_in X a b).
We will prove closed_in X Tx (closed_interval_in X a b).
Apply (closed_inI X Tx (closed_interval_in X a b)) to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume Hx: x ∈ closed_interval_in X a b.
We will prove 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).
Set U to be the term (open_ray_lower X a) ∪ (open_ray_upper X b).
We use U to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HUaSub: open_ray_lower X a ∈ open_rays_subbasis X.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis X a HaX).
We prove the intermediate claim HUbSub: open_ray_upper X b ∈ open_rays_subbasis X.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis X b HbX).
We prove the intermediate claim HUaTx: open_ray_lower X a ∈ Tx.
An exact proof term for the current goal is ((open_rays_subbasis_sub_order_topology X Hso) (open_ray_lower X a) HUaSub).
We prove the intermediate claim HUbTx: open_ray_upper X b ∈ Tx.
An exact proof term for the current goal is ((open_rays_subbasis_sub_order_topology X Hso) (open_ray_upper X b) HUbSub).
An exact proof term for the current goal is (topology_binunion_closed X Tx (open_ray_lower X a) (open_ray_upper X b) HTx HUaTx HUbTx).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closed_interval_in X a b.
We will prove x ∈ X ∖ U.
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 Hcond: (x = a ∨ order_rel X a x) ∧ (x = b ∨ order_rel X x b).
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ (x0 = a ∨ order_rel X a x0) ∧ (x0 = b ∨ order_rel X x0 b)) x Hx).
We prove the intermediate claim Hleft: x = a ∨ order_rel X a x.
An exact proof term for the current goal is (andEL (x = a ∨ order_rel X a x) (x = b ∨ order_rel X x b) Hcond).
We prove the intermediate claim Hright: x = b ∨ order_rel X x b.
An exact proof term for the current goal is (andER (x = a ∨ order_rel X a x) (x = b ∨ order_rel X x b) Hcond).
We prove the intermediate claim HnotLower: ¬ (order_rel X x a).
Apply Hleft to the current goal.
Assume Heq: x = a.
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is (order_rel_irref X a).
Assume Hax: order_rel X a x.
Assume Hxa: order_rel X x a.
We prove the intermediate claim Haa: order_rel X a a.
An exact proof term for the current goal is (order_rel_trans X a x a Hso HaX HxX HaX Hax Hxa).
An exact proof term for the current goal is ((order_rel_irref X a) Haa).
We prove the intermediate claim HnotUpper: ¬ (order_rel X b x).
Apply Hright to the current goal.
Assume Heq: x = b.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (order_rel_irref X b).
Assume Hxb: order_rel X x b.
Assume Hbx: order_rel X b x.
We prove the intermediate claim Hbb: order_rel X b b.
An exact proof term for the current goal is (order_rel_trans X b x b Hso HbX HxX HbX Hbx Hxb).
An exact proof term for the current goal is ((order_rel_irref X b) Hbb).
Apply (setminusI X U x HxX) to the current goal.
Assume HxU: x ∈ U.
Apply (binunionE (open_ray_lower X a) (open_ray_upper X b) x HxU) to the current goal.
Assume HxLow: x ∈ open_ray_lower X a.
We prove the intermediate claim Hxa: order_rel X x a.
An exact proof term for the current goal is (SepE2 X (λt : set ⇒ order_rel X t a) x HxLow).
An exact proof term for the current goal is (HnotLower Hxa).
Assume HxUp: x ∈ open_ray_upper X b.
We prove the intermediate claim Hbx: order_rel X b x.
An exact proof term for the current goal is (SepE2 X (λt : set ⇒ order_rel X b t) x HxUp).
An exact proof term for the current goal is (HnotUpper Hbx).
Let x be given.
Assume Hx: x ∈ X ∖ U.
We will prove x ∈ closed_interval_in X a b.
We prove the intermediate claim Hxpair: x ∈ X ∧ x ∉ U.
An exact proof term for the current goal is (setminusE X U x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (andEL (x ∈ X) (x ∉ U) Hxpair).
We prove the intermediate claim HxNotU: x ∉ U.
An exact proof term for the current goal is (andER (x ∈ X) (x ∉ U) Hxpair).
We prove the intermediate claim HnotLowSet: ¬ (x ∈ open_ray_lower X a).
Assume HxLow: x ∈ open_ray_lower X a.
An exact proof term for the current goal is (HxNotU (binunionI1 (open_ray_lower X a) (open_ray_upper X b) x HxLow)).
We prove the intermediate claim HnotUpSet: ¬ (x ∈ open_ray_upper X b).
Assume HxUp: x ∈ open_ray_upper X b.
An exact proof term for the current goal is (HxNotU (binunionI2 (open_ray_lower X a) (open_ray_upper X b) x HxUp)).
We prove the intermediate claim HnotLower: ¬ (order_rel X x a).
Assume Hxa: order_rel X x a.
We prove the intermediate claim HxLow: x ∈ open_ray_lower X a.
An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X t a) x HxX Hxa).
An exact proof term for the current goal is (HnotLowSet HxLow).
We prove the intermediate claim HnotUpper: ¬ (order_rel X b x).
Assume Hbx: order_rel X b x.
We prove the intermediate claim HxUp: x ∈ open_ray_upper X b.
An exact proof term for the current goal is (SepI X (λt : set ⇒ order_rel X b t) x HxX Hbx).
An exact proof term for the current goal is (HnotUpSet HxUp).
We prove the intermediate claim Hleft: x = a ∨ order_rel X a x.
Apply (order_rel_trichotomy_or_impred X x a Hso HxX HaX (x = a ∨ order_rel X a x)) to the current goal.
Assume Hxa: order_rel X x a.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotLower Hxa).
Assume Heq: x = a.
An exact proof term for the current goal is (orIL (x = a) (order_rel X a x) Heq).
Assume Hax: order_rel X a x.
An exact proof term for the current goal is (orIR (x = a) (order_rel X a x) Hax).
We prove the intermediate claim Hright: x = b ∨ order_rel X x b.
Apply (order_rel_trichotomy_or_impred X x b Hso HxX HbX (x = b ∨ order_rel X x b)) to the current goal.
Assume Hxb: order_rel X x b.
An exact proof term for the current goal is (orIR (x = b) (order_rel X x b) Hxb).
Assume Heq: x = b.
An exact proof term for the current goal is (orIL (x = b) (order_rel X x b) Heq).
Assume Hbx: order_rel X b x.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotUpper Hbx).
We prove the intermediate claim Hdef: closed_interval_in X a b = {x0 ∈ X|(x0 = a ∨ order_rel X a x0) ∧ (x0 = b ∨ order_rel X x0 b)}.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ (x0 = a ∨ order_rel X a x0) ∧ (x0 = b ∨ order_rel X x0 b)) x HxX (andI (x = a ∨ order_rel X a x) (x = b ∨ order_rel X x b) Hleft Hright)).
An exact proof term for the current goal is (closure_subset_of_closed_superset X Tx (order_interval X a b) (closed_interval_in X a b) HTx Hsub Hclosed).
∎