∀x,y:ℝ.  (x ≠ y 
⇐⇒ r0 < |x - y|)
{ Auto }
1. x : ℝ
2. y : ℝ
3. x ≠ y
⊢ r0 < |x - y|
1. x : ℝ
2. y : ℝ
3. r0 < |x - y|
⊢ x ≠ y