---

Step * of Lemma qless_transitivity

∀[a,b,c:ℚ].  (a < c) supposing (b < c and a < b)
BY
{ (InstLemma `qless_trans_qorder` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[a,b,c:\mBbbQ{}].    (a  <  c)  supposing  (b  <  c  and  a  <  b)


By

---

Latex:
(InstLemma  `qless\_trans\_qorder`  []  THEN  Trivial)

---

Home Index