Let x be given.

We will prove x ∈ Empty.

We prove the intermediate claim HxLo: x ∈ closed_interval (minus_SNo 1) (minus_SNo one_third).

We prove the intermediate claim HxHi: x ∈ closed_interval one_third 1.

An exact proof term for the current goal is (binintersectE1 (closed_interval one_third 1) (closed_interval (minus_SNo 1) 1) x HxI3).

Use reflexivity.

We prove the intermediate claim HxLo': x ∈ {t ∈ R|¬ (Rlt t (minus_SNo 1)) ∧ ¬ (Rlt (minus_SNo one_third) t)}.

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

An exact proof term for the current goal is HxLo.

We prove the intermediate claim HxR: x ∈ R.

An exact proof term for the current goal is (SepE1 R (λt : set ⇒ ¬ (Rlt t (minus_SNo 1)) ∧ ¬ (Rlt (minus_SNo one_third) t)) x HxLo').

We prove the intermediate claim HxLoConj: ¬ (Rlt x (minus_SNo 1)) ∧ ¬ (Rlt (minus_SNo one_third) x).

An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t (minus_SNo 1)) ∧ ¬ (Rlt (minus_SNo one_third) t)) x HxLo').

We prove the intermediate claim Hnlt_m13_x: ¬ (Rlt (minus_SNo one_third) x).

An exact proof term for the current goal is (andER (¬ (Rlt x (minus_SNo 1))) (¬ (Rlt (minus_SNo one_third) x)) HxLoConj).

We prove the intermediate claim HHi_def: closed_interval one_third 1 = {t ∈ R|¬ (Rlt t one_third) ∧ ¬ (Rlt 1 t)}.

Use reflexivity.

We prove the intermediate claim HxHi': x ∈ {t ∈ R|¬ (Rlt t one_third) ∧ ¬ (Rlt 1 t)}.

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

An exact proof term for the current goal is HxHi.

We prove the intermediate claim HxHiConj: ¬ (Rlt x one_third) ∧ ¬ (Rlt 1 x).

An exact proof term for the current goal is (SepE2 R (λt : set ⇒ ¬ (Rlt t one_third) ∧ ¬ (Rlt 1 t)) x HxHi').

We prove the intermediate claim Hnlt_x_13: ¬ (Rlt x one_third).

An exact proof term for the current goal is (andEL (¬ (Rlt x one_third)) (¬ (Rlt 1 x)) HxHiConj).

We prove the intermediate claim H13R: one_third ∈ R.

An exact proof term for the current goal is one_third_in_R.

We prove the intermediate claim Hm13R: (minus_SNo one_third) ∈ R.

An exact proof term for the current goal is (real_minus_SNo one_third H13R).

We prove the intermediate claim H13lex: Rle one_third x.

An exact proof term for the current goal is (RleI one_third x H13R HxR Hnlt_x_13).

We prove the intermediate claim Hxlem13: Rle x (minus_SNo one_third).

An exact proof term for the current goal is (RleI x (minus_SNo one_third) HxR Hm13R Hnlt_m13_x).

We prove the intermediate claim H13lem13: Rle one_third (minus_SNo one_third).

An exact proof term for the current goal is (Rle_tra one_third x (minus_SNo one_third) H13lex Hxlem13).

Apply FalseE to the current goal.

An exact proof term for the current goal is ((RleE_nlt one_third (minus_SNo one_third) H13lem13) (Rlt_minus_one_third_one_third)).