We will prove False.

Set X to be the term two_by_nat.

Set B to be the term order_topology_basis X.

Set U to be the term {(1,0)}.

We prove the intermediate claim Hneigh: ∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ B, x ∈ b ∧ b ⊆ U0) U Hopen).

We prove the intermediate claim HxU: (1,0) ∈ U.

An exact proof term for the current goal is (SingI (1,0)).

We prove the intermediate claim Hexb: ∃b ∈ B, (1,0) ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (Hneigh (1,0) HxU).

Apply Hexb to the current goal.

Let b be given.

Assume Hbpair.

Apply Hbpair to the current goal.

Assume HbB: b ∈ B.

Assume Hbcore: (1,0) ∈ b ∧ b ⊆ U.

We prove the intermediate claim HbcU: b ⊆ U.

An exact proof term for the current goal is (andER ((1,0) ∈ b) (b ⊆ U) Hbcore).

We prove the intermediate claim HUcb: U ⊆ b.

Let y be given.

Assume Hy: y ∈ U.

We will prove y ∈ b.

We prove the intermediate claim HyEq: y = (1,0).

An exact proof term for the current goal is (SingE (1,0) y Hy).

rewrite the current goal using HyEq (from left to right).

An exact proof term for the current goal is (andEL ((1,0) ∈ b) (b ⊆ U) Hbcore).

We prove the intermediate claim HbeqU: b = U.

Apply set_ext to the current goal.

Let y be given.

Assume Hy: y ∈ b.

An exact proof term for the current goal is (HbcU y Hy).

Let y be given.

Assume Hy: y ∈ U.

An exact proof term for the current goal is (HUcb y Hy).

We prove the intermediate claim HUnotB: U ∉ B.

An exact proof term for the current goal is two_by_nat_singleton_not_in_basis.

We prove the intermediate claim HUinB: U ∈ B.

rewrite the current goal using HbeqU (from right to left).

An exact proof term for the current goal is HbB.

An exact proof term for the current goal is (HUnotB HUinB).

∎