---

Step * 1 of Lemma rneq-rat2real


1. q1 : ℚ
2. q2 : ℚ
⊢ uiff(q1 < q2 ∨ q2 < q1;¬(q1 = q2 ∈ ℚ))
BY
{ ((InstLemma `qless_trichot_qorder` [⌜q1⌝;⌜q2⌝]⋅ THENA Auto) THEN SplitOrHyps THEN Auto) }

1
1. q1 : ℚ
2. q2 : ℚ
3. q1 = q2 ∈ ℚ
4. q1 < q2 ∨ q2 < q1
⊢ ¬(q1 = q2 ∈ ℚ)

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `qless\_trichot\_qorder`  [\mkleeneopen{}q1\mkleeneclose{};\mkleeneopen{}q2\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  SplitOrHyps  THEN  Auto)

---

Home Index