Elimination of the quantifier ∃in ∃x, φ

In order to inherit properties of finite open segment set ]a,b[ where a, b are real numbers, we split the problem of existence of x:
∃x, φ is rewritten ∃x, x < -1, φ

or φ(x := -1)

or ∃x ∈ ]-1, 1[, φ

or φ(x := 1) or ∃x, x > 1, φ.


As the application y → 1/y is bijective from ]-1, 0[ to ]-∞, -1[ and from ]0, 1[ to ]1, +∞[,
∃x, φ is rewritten ∃y ∈ ]-1, 0[, φ(x := 1/y)

or φ(x := -1)

or ∃x∈ ]-1, 1[, φ

or φ(x := 1)

or ∃y ∈ ]0, 1[, φ(x := 1/y).
By φ(x := 1/y) we mean that we replace each occurence of x by 1/y... we then obtain a rational expressions. By multiplying by yn, where n is large enough, we obtain polynomial expressions.
∃x, x² + 3x + 2 = 0 is rewritten ∃y ∈ ]-1, 0[, 1 + 3y + 2y² = 0

or (-1)² + 3(-1) + 2 = 0

or ∃x∈ ]-1, 1[, x² + 3x + 2 = 0

or (1)² + 3 + 2 = 0

or ∃y ∈ ]0, 1[, 1 + 3y + 2y² = 0.