We will prove ex50_R3_ones ∈ euclidean_space 3.

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

Let i be given.

An exact proof term for the current goal is real_1.

∎