Let X be given.
We will prove open_rays_subbasis X ⊆ đ’Ģ X.
Let I be given.
Assume HI: I ∈ open_rays_subbasis X.
We will prove I ∈ đ’Ģ X.
Apply (binunionE' ({I0 ∈ đ’Ģ X|∃a ∈ X, I0 = open_ray_upper X a} âˆĒ {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = open_ray_lower X b}) {X} I (I ∈ đ’Ģ X)) to the current goal.
Assume HI0: I ∈ ({I0 ∈ đ’Ģ X|∃a ∈ X, I0 = open_ray_upper X a} âˆĒ {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = open_ray_lower X b}).
Apply (binunionE' {I0 ∈ đ’Ģ X|∃a ∈ X, I0 = open_ray_upper X a} {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = open_ray_lower X b} I (I ∈ đ’Ģ X)) to the current goal.
Assume HI1: I ∈ {I0 ∈ đ’Ģ X|∃a ∈ X, I0 = open_ray_upper X a}.
An exact proof term for the current goal is (SepE1 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, I0 = open_ray_upper X a) I HI1).
Assume HI2: I ∈ {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = open_ray_lower X b}.
An exact proof term for the current goal is (SepE1 (đ’Ģ X) (ÎģI0 : set ⇒ ∃b ∈ X, I0 = open_ray_lower X b) I HI2).
An exact proof term for the current goal is HI0.
Assume HIX: I ∈ {X}.
We prove the intermediate claim HIEq: I = X.
An exact proof term for the current goal is (SingE X I HIX).
rewrite the current goal using HIEq (from left to right).
An exact proof term for the current goal is (Self_In_Power X).
An exact proof term for the current goal is HI.
∎