English
If there exists an element a in l with p a, then choose p l hp is an element of l and satisfies p.
Русский
Если существует элемент a в l, такой что p a, то choose p l hp является элементом l и удовлетворяет p.
LaTeX
$$$ \\exists a\\ a\\in l \\land p a \\Rightarrow (\\text{choose } p l hp) \\in l \\land p (\\text{choose } p l hp) $$$
Lean4
theorem choose_spec (hp : ∃ a, a ∈ l ∧ p a) : choose p l hp ∈ l ∧ p (choose p l hp) :=
(chooseX p l hp).property