1. r : ℚ
2. 0 < |r|
⊢ ¬(r = 0 ∈ ℚ)
{ (D 0 THEN Auto) }
3. r = 0 ∈ ℚ
⊢ False