Let X, U and y be given.
Assume Hso: simply_ordered_set X.
Assume HU: U ∈ order_topology X.
Assume HyU: y ∈ U.
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 HUopen: open_in X (order_topology X) U.
An exact proof term for the current goal is (andI (topology_on X (order_topology X)) (U ∈ order_topology X) HTx HU).
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).
Set Fam to be the term {b ∈ order_topology_basis X|b ⊆ U}.
We prove the intermediate claim HUeq: U = ⋃ Fam.
An exact proof term for the current goal is (open_as_union_of_basis_elements X (order_topology_basis X) HBasis U HUopen).
We prove the intermediate claim HyUnion: y ∈ ⋃ Fam.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HyU.
Apply UnionE_impred Fam y HyUnion to the current goal.
Let b be given.
Assume Hyb: y ∈ b.
Assume HbFam: b ∈ Fam.
We use b to witness the existential quantifier.
We will prove b ∈ order_topology_basis X ∧ (y ∈ b ∧ b ⊆ U).
We prove the intermediate claim HbB: b ∈ order_topology_basis X.
An exact proof term for the current goal is (SepE1 (order_topology_basis X) (λb0 : set ⇒ b0 ⊆ U) b HbFam).
We prove the intermediate claim Hbsub: b ⊆ U.
An exact proof term for the current goal is (SepE2 (order_topology_basis X) (λb0 : set ⇒ b0 ⊆ U) b HbFam).
Apply andI to the current goal.
An exact proof term for the current goal is HbB.
Apply andI to the current goal.
An exact proof term for the current goal is Hyb.
An exact proof term for the current goal is Hbsub.
∎