Assume Hsub: Empty ⊆ R.

We prove the intermediate claim Hreq: R ∖ Empty = R.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ R ∖ Empty.

An exact proof term for the current goal is (setminusE1 R Empty x Hx).

Let x be given.

Assume HxR: x ∈ R.

An exact proof term for the current goal is (setminusI R Empty x HxR (EmptyE x)).

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

Let X and y be given.

Assume HFinX HyNot HXind.

Assume HsubXY: (X ∪ {y}) ⊆ R.

We prove the intermediate claim HsubX: X ⊆ R.

Let z be given.

Assume HzX: z ∈ X.

An exact proof term for the current goal is (HsubXY z (binunionI1 X {y} z HzX)).

We prove the intermediate claim HyR: y ∈ R.

An exact proof term for the current goal is (HsubXY y (binunionI2 X {y} y (SingI y))).

We prove the intermediate claim HXopen: R ∖ X ∈ R_standard_topology.

An exact proof term for the current goal is (HXind HsubX).

We prove the intermediate claim Hyopen: R ∖ {y} ∈ R_standard_topology.

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

An exact proof term for the current goal is (R_minus_singleton_in_R_standard_topology y HyR).

We prove the intermediate claim Hdecomp: R ∖ (X ∪ {y}) = (R ∖ X) ∩ (R ∖ {y}).

An exact proof term for the current goal is (setminus_binunion_eq_binintersect R X {y}).

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