Let X, d, x and r be given.

Apply PowerI to the current goal.

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

∎