∀x:ℝ. (x ≠ r0 
 (r0 < x^2))
{ (Auto THEN D -1) }
1. x : ℝ
2. x < r0
⊢ r0 < x^2
2. r0 < x