Let X, d, x and r be given.

Let y be given.

Assume Hy: y ∈ open_ball X d x r.

An exact proof term for the current goal is (open_ballE1 X d x r y Hy).

∎