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