---

Step * of Lemma rneq-rat2real

∀q1,q2:ℚ.  uiff(rat2real(q1) ≠ rat2real(q2);¬(q1 = q2 ∈ ℚ))
BY
{ ((UnivCD THENA Auto) THEN Unfold `rneq` 0 THEN (RWO "rless-rat2real" 0 THENA Auto)) }

1
1. q1 : ℚ
2. q2 : ℚ
⊢ uiff(q1 < q2 ∨ q2 < q1;¬(q1 = q2 ∈ ℚ))

---

Latex:

---

Latex:
\mforall{}q1,q2:\mBbbQ{}.    uiff(rat2real(q1)  \mneq{}  rat2real(q2);\mneg{}(q1  =  q2))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `rneq`  0  THEN  (RWO  "rless-rat2real"  0  THENA  Auto))

---

Home Index