∀x:ℝ. (x^2 < r1 
 |x| < r1)
{ Auto }
1. x : ℝ
2. x^2 < r1
⊢ |x| < r1
2. |x| < r1
⊢ x^2 < r1