---

Step * of Lemma q_trichotomy

∀r:ℚ. ((↑qpositive(r)) ∨ (r = 0 ∈ ℚ) ∨ (↑qpositive(-(r))))
BY
{ xxx(Auto THEN QArith)xxx }

---

Latex:

---

Latex:
\mforall{}r:\mBbbQ{}.  ((\muparrow{}qpositive(r))  \mvee{}  (r  =  0)  \mvee{}  (\muparrow{}qpositive(-(r))))


By

---

Latex:
xxx(Auto  THEN  QArith)xxx

---

Home Index