∀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