---

Step * 1 1 of Lemma rneq-rat2real


1. q1 : ℚ
2. q2 : ℚ
3. q1 = q2 ∈ ℚ
4. q1 < q2 ∨ q2 < q1
⊢ ¬(q1 = q2 ∈ ℚ)
BY
{ (D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  q1  :  \mBbbQ{}
2.  q2  :  \mBbbQ{}
3.  q1  =  q2
4.  q1  <  q2  \mvee{}  q2  <  q1
\mvdash{}  \mneg{}(q1  =  q2)


By

---

Latex:
(D  -1  THEN  Auto)

---

Home Index