1. s : ℚ
2. ¬(s = 0 ∈ ℚ)
3. ¬(s = 0 ∈ ℚ)
4. ¬(|s| = 0 ∈ ℚ)
⊢ |1/s| = 1/|s| ∈ ℚ
{ RepeatFor 2 (MoveToConcl (-1)) }
⊢ (¬(s = 0 ∈ ℚ))
(¬(|s| = 0 ∈ ℚ))
(|1/s| = 1/|s| ∈ ℚ)