We will prove ex50_R3_zero ∈ euclidean_space 3.

Apply (graph3_in_euclidean_space3 (λ_ : set ⇒ 0)) to the current goal.

Let i be given.

An exact proof term for the current goal is real_0.

∎