---

Step * of Lemma qle_connex

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

1
1. a : ℚ@i
2. b : ℚ@i
3. a < b
⊢ a ≤ b

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

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbQ{}.    ((a  \mleq{}  b)  \mvee{}  (b  \mleq{}  a))


By

---

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

---

Home Index