---

Step * of Lemma qle-iff

∀a,b:ℚ.  uiff(a ≤ b;a < b ∨ (a = b ∈ ℚ))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `qless_trichot_qorder` [⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN (InstLemma `qless_complement_qorder` [⌜b⌝;⌜a⌝]⋅ THENA Auto)) }

1
1. a : ℚ@i
2. b : ℚ@i
3. a < b ∨ (a = b ∈ ℚ) ∨ b < a
4. uiff(¬a < b;b ≤ a)
⊢ uiff(a ≤ b;a < b ∨ (a = b ∈ ℚ))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbQ{}.    uiff(a  \mleq{}  b;a  <  b  \mvee{}  (a  =  b))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `qless\_trichot\_qorder`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `qless\_complement\_qorder`  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index