---

Step * 1 2 1 1 of Lemma qadd_grp_wf2


1. a : ℚ
⊢ (↑qpositive(a + -(a))) ∨ (a = a ∈ ℚ)
BY
{ (OrRight THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
\mvdash{}  (\muparrow{}qpositive(a  +  -(a)))  \mvee{}  (a  =  a)


By

---

Latex:
(OrRight  THEN  Auto)\mcdot{}

---

Home Index