Let c and r be given.
Assume Hc: c ∈ EuclidPlane.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ open_ball EuclidPlane EuclidPlane_metric c r.
We will prove p ∈ {p0 ∈ EuclidPlane|Rlt (distance_R2 p0 c) r}.
We prove the intermediate claim HpE: p ∈ EuclidPlane.
An exact proof term for the current goal is (open_ballE1 EuclidPlane EuclidPlane_metric c r p Hp).
We prove the intermediate claim Hlt: Rlt (apply_fun EuclidPlane_metric (c,p)) r.
An exact proof term for the current goal is (open_ballE2 EuclidPlane EuclidPlane_metric c r p Hp).
We prove the intermediate claim Hcp: apply_fun EuclidPlane_metric (c,p) = distance_R2 c p.
An exact proof term for the current goal is (EuclidPlane_metric_apply c p Hc HpE).
We prove the intermediate claim Hsym: distance_R2 c p = distance_R2 p c.
An exact proof term for the current goal is (distance_R2_sym c p Hc HpE).
We prove the intermediate claim Hltcp: Rlt (distance_R2 c p) r.
rewrite the current goal using Hcp (from right to left).
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hltpc: Rlt (distance_R2 p c) r.
rewrite the current goal using Hsym (from right to left).
An exact proof term for the current goal is Hltcp.
An exact proof term for the current goal is (SepI EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 c) r) p HpE Hltpc).
Let p be given.
Assume Hp: p ∈ {p0 ∈ EuclidPlane|Rlt (distance_R2 p0 c) r}.
We will prove p ∈ open_ball EuclidPlane EuclidPlane_metric c r.
We prove the intermediate claim HpE: p ∈ EuclidPlane.
An exact proof term for the current goal is (SepE1 EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 c) r) p Hp).
We prove the intermediate claim Hltpc: Rlt (distance_R2 p c) r.
An exact proof term for the current goal is (SepE2 EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 c) r) p Hp).
We prove the intermediate claim Hsym: distance_R2 p c = distance_R2 c p.
An exact proof term for the current goal is (distance_R2_sym p c HpE Hc).
We prove the intermediate claim Hltcp: Rlt (distance_R2 c p) r.
rewrite the current goal using Hsym (from right to left).
An exact proof term for the current goal is Hltpc.
We prove the intermediate claim Hcp: apply_fun EuclidPlane_metric (c,p) = distance_R2 c p.
An exact proof term for the current goal is (EuclidPlane_metric_apply c p Hc HpE).
We prove the intermediate claim Hlt: Rlt (apply_fun EuclidPlane_metric (c,p)) r.
rewrite the current goal using Hcp (from left to right).
An exact proof term for the current goal is Hltcp.
An exact proof term for the current goal is (open_ballI EuclidPlane EuclidPlane_metric c r p HpE Hlt).
∎