Let f be given.

We will prove f ∈ Empty.

We prove the intermediate claim Hb: f ∈ bounded_sequences_Romega.

We prove the intermediate claim Hu: f ∈ unbounded_sequences_Romega.

We prove the intermediate claim Hbprop: bounded_sequence_Romega f.

An exact proof term for the current goal is (SepE2 R_omega_space (λf0 : set ⇒ bounded_sequence_Romega f0) f Hb).

We prove the intermediate claim Huprop: unbounded_sequence_Romega f.

An exact proof term for the current goal is (SepE2 R_omega_space (λf0 : set ⇒ unbounded_sequence_Romega f0) f Hu).

Apply Hbprop to the current goal.

Let M be given.

Assume HMconj.

We prove the intermediate claim HMR: M ∈ R.

An exact proof term for the current goal is (andEL (M ∈ R) (∀n : set, n ∈ ω → apply_fun f n ∈ open_interval (minus_SNo M) M) HMconj).

We prove the intermediate claim Hbnd: ∀n : set, n ∈ ω → apply_fun f n ∈ open_interval (minus_SNo M) M.

An exact proof term for the current goal is (andER (M ∈ R) (∀n : set, n ∈ ω → apply_fun f n ∈ open_interval (minus_SNo M) M) HMconj).

We prove the intermediate claim Hexn: ∃n ∈ ω, ¬ (apply_fun f n ∈ open_interval (minus_SNo M) M).

An exact proof term for the current goal is (Huprop M HMR).

Apply Hexn to the current goal.

Let n be given.

Assume Hnconj.

We prove the intermediate claim HnO: n ∈ ω.

An exact proof term for the current goal is (andEL (n ∈ ω) (¬ (apply_fun f n ∈ open_interval (minus_SNo M) M)) Hnconj).

We prove the intermediate claim Hnnot: ¬ (apply_fun f n ∈ open_interval (minus_SNo M) M).

An exact proof term for the current goal is (andER (n ∈ ω) (¬ (apply_fun f n ∈ open_interval (minus_SNo M) M)) Hnconj).

We prove the intermediate claim Hfalse: False.

An exact proof term for the current goal is (Hnnot (Hbnd n HnO)).

An exact proof term for the current goal is (FalseE Hfalse (f ∈ Empty)).