Let X be given.
We will prove subbasis_on X (open_rays_subbasis X).
We will prove (open_rays_subbasis X ⊆ 𝒫 X) ∧ ⋃ (open_rays_subbasis X) = X.
Apply andI to the current goal.
An exact proof term for the current goal is (open_rays_subbasis_sub_Power X).
Apply set_ext to the current goal.
Let x be given.
Assume HxU: x ∈ ⋃ (open_rays_subbasis X).
We will prove x ∈ X.
Apply (UnionE_impred (open_rays_subbasis X) x HxU) to the current goal.
Let U be given.
Assume HxUin: x ∈ U.
Assume HU: U ∈ open_rays_subbasis X.
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
An exact proof term for the current goal is (open_rays_subbasis_sub_Power X U HU).
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (PowerE X U HUpow).
An exact proof term for the current goal is (HUsub x HxUin).
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ ⋃ (open_rays_subbasis X).
We prove the intermediate claim HXInS: X ∈ open_rays_subbasis X.
An exact proof term for the current goal is (binunionI2 ({I0 ∈ 𝒫 X|∃a ∈ X, I0 = open_ray_upper X a} ∪ {I0 ∈ 𝒫 X|∃b ∈ X, I0 = open_ray_lower X b}) {X} X (SingI X)).
An exact proof term for the current goal is (UnionI (open_rays_subbasis X) x X HxX HXInS).
∎