We will prove closed_in (closed_interval (minus_SNo 1) 1) (closed_interval_topology (minus_SNo 1) 1) ((closed_interval (minus_SNo 1) (minus_SNo one_third)) ∩ (closed_interval (minus_SNo 1) 1)).
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim Hm1real: (minus_SNo 1) ∈ real.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim Hm1R: (minus_SNo 1) ∈ R.
rewrite the current goal using HdefR (from left to right) at position 1.
An exact proof term for the current goal is Hm1real.
We prove the intermediate claim H1R: 1 ∈ R.
rewrite the current goal using HdefR (from left to right) at position 1.
An exact proof term for the current goal is real_1.
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 H13real: one_third ∈ real.
rewrite the current goal using HdefR (from right to left) at position 1.
An exact proof term for the current goal is H13R.
We prove the intermediate claim Hm13real: (minus_SNo one_third) ∈ real.
An exact proof term for the current goal is (real_minus_SNo one_third H13real).
We prove the intermediate claim Hm13R: (minus_SNo one_third) ∈ R.
rewrite the current goal using HdefR (from left to right) at position 1.
An exact proof term for the current goal is Hm13real.
An exact proof term for the current goal is (closed_interval_closed_in_closed_interval_topology (minus_SNo 1) 1 (minus_SNo 1) (minus_SNo one_third) Hm1R H1R Hm1R Hm13R).
∎