Let X, a and b be given.
Assume Hso: simply_ordered_set X.
Assume HaX: a ∈ X.
Assume HbX: b ∈ X.
We will prove order_interval X a b ∈ order_topology X.
We prove the intermediate claim HTx: topology_on X (order_topology X).
An exact proof term for the current goal is (order_topology_is_topology X Hso).
We prove the intermediate claim HU: {x ∈ X|order_rel X a x} ∈ order_topology X.
Set U to be the term open_ray_upper X a.
We prove the intermediate claim HUinB: U ∈ order_topology_basis X.
An exact proof term for the current goal is (open_ray_upper_in_order_topology_basis X a HaX).
We prove the intermediate claim HBasis: basis_on X (order_topology_basis X).
An exact proof term for the current goal is (order_topology_basis_is_basis X Hso).
An exact proof term for the current goal is (basis_in_generated X (order_topology_basis X) U HBasis HUinB).
We prove the intermediate claim HV: {x ∈ X|order_rel X x b} ∈ order_topology X.
Set V to be the term open_ray_lower X b.
We prove the intermediate claim HVinB: V ∈ order_topology_basis X.
An exact proof term for the current goal is (open_ray_lower_in_order_topology_basis X b HbX).
We prove the intermediate claim HBasis: basis_on X (order_topology_basis X).
An exact proof term for the current goal is (order_topology_basis_is_basis X Hso).
An exact proof term for the current goal is (basis_in_generated X (order_topology_basis X) V HBasis HVinB).
We prove the intermediate claim Heq: order_interval X a b = ({x ∈ X|order_rel X a x} ∩ {x ∈ X|order_rel X x b}).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ order_interval X a b.
We will prove x ∈ ({x0 ∈ X|order_rel X a x0} ∩ {x0 ∈ X|order_rel X x0 b}).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) x Hx).
We prove the intermediate claim Hconj: order_rel X a x ∧ order_rel X x b.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) x Hx).
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) Hconj).
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) Hconj).
We prove the intermediate claim HxU: x ∈ {x0 ∈ X|order_rel X a x0}.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0) x HxX Hax).
We prove the intermediate claim HxV: x ∈ {x0 ∈ X|order_rel X x0 b}.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 b) x HxX Hxb).
An exact proof term for the current goal is (binintersectI {x0 ∈ X|order_rel X a x0} {x0 ∈ X|order_rel X x0 b} x HxU HxV).
Let x be given.
Assume Hx: x ∈ ({x0 ∈ X|order_rel X a x0} ∩ {x0 ∈ X|order_rel X x0 b}).
We will prove x ∈ order_interval X a b.
We prove the intermediate claim HxU: x ∈ {x0 ∈ X|order_rel X a x0}.
An exact proof term for the current goal is (binintersectE1 {x0 ∈ X|order_rel X a x0} {x0 ∈ X|order_rel X x0 b} x Hx).
We prove the intermediate claim HxV: x ∈ {x0 ∈ X|order_rel X x0 b}.
An exact proof term for the current goal is (binintersectE2 {x0 ∈ X|order_rel X a x0} {x0 ∈ X|order_rel X x0 b} x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X a x0) x HxU).
We prove the intermediate claim Hax: order_rel X a x.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0) x HxU).
We prove the intermediate claim Hxb: order_rel X x b.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 b) x HxV).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) x HxX (andI (order_rel X a x) (order_rel X x b) Hax Hxb)).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed X (order_topology X) {x ∈ X|order_rel X a x} {x ∈ X|order_rel X x b} HTx HU HV).
∎