∀[x,y:ℝ].  ((x)* < (y)* ⇐⇒ x < y){ Auto }1. [x] : ℝ2. [y] : ℝ3. (x)* < (y)*⊢ x < y1. [x] : ℝ2. [y] : ℝ3. x < y⊢ (x)* < (y)*