Let U and V be given.
Assume HU HV.
We will prove U ∪ V ∈ R_standard_topology.
We prove the intermediate claim HUpow: U ∈ 𝒫 R.
An exact proof term for the current goal is (SepE1 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HU).
We prove the intermediate claim HVpow: V ∈ 𝒫 R.
An exact proof term for the current goal is (SepE1 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) V HV).
We prove the intermediate claim HUprop: ∀x ∈ U, ∃b0 ∈ R_standard_basis, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HU).
We prove the intermediate claim HVprop: ∀x ∈ V, ∃b0 ∈ R_standard_basis, x ∈ b0 ∧ b0 ⊆ V.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) V HV).
We prove the intermediate claim HUVpow: U ∪ V ∈ 𝒫 R.
Apply PowerI to the current goal.
Let x be given.
Assume HxUV: x ∈ U ∪ V.
Apply (binunionE U V x HxUV) to the current goal.
Assume HxU: x ∈ U.
An exact proof term for the current goal is (PowerE R U HUpow x HxU).
Assume HxV: x ∈ V.
An exact proof term for the current goal is (PowerE R V HVpow x HxV).
We prove the intermediate claim HUVprop: ∀x ∈ U ∪ V, ∃b0 ∈ R_standard_basis, x ∈ b0 ∧ b0 ⊆ U ∪ V.
Let x be given.
Assume HxUV: x ∈ U ∪ V.
Apply (binunionE U V x HxUV) to the current goal.
Assume HxU: x ∈ U.
We prove the intermediate claim Hexb: ∃b0 ∈ R_standard_basis, x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (HUprop x HxU).
Apply Hexb to the current goal.
Let b0 be given.
Assume Hb0pair.
We use b0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (b0 ∈ R_standard_basis) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).
We prove the intermediate claim Hb0prop: x ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (andER (b0 ∈ R_standard_basis) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ U) Hb0prop).
We prove the intermediate claim Hb0subU: b0 ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ U) Hb0prop).
Let y be given.
Assume Hyb0.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (Hb0subU y Hyb0).
An exact proof term for the current goal is (binunionI1 U V y HyU).
Assume HxV: x ∈ V.
We prove the intermediate claim Hexb: ∃b0 ∈ R_standard_basis, x ∈ b0 ∧ b0 ⊆ V.
An exact proof term for the current goal is (HVprop x HxV).
Apply Hexb to the current goal.
Let b0 be given.
Assume Hb0pair.
We use b0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (b0 ∈ R_standard_basis) (x ∈ b0 ∧ b0 ⊆ V) Hb0pair).
We prove the intermediate claim Hb0prop: x ∈ b0 ∧ b0 ⊆ V.
An exact proof term for the current goal is (andER (b0 ∈ R_standard_basis) (x ∈ b0 ∧ b0 ⊆ V) Hb0pair).
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (x ∈ b0) (b0 ⊆ V) Hb0prop).
We prove the intermediate claim Hb0subV: b0 ⊆ V.
An exact proof term for the current goal is (andER (x ∈ b0) (b0 ⊆ V) Hb0prop).
Let y be given.
Assume Hyb0.
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (Hb0subV y Hyb0).
An exact proof term for the current goal is (binunionI2 U V y HyV).
An exact proof term for the current goal is (SepI (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) (U ∪ V) HUVpow HUVprop).
∎