---

Step * of Lemma qless_irreflexivity

∀[a:ℚ]. False supposing a < a
BY
{ (InstLemma `qless_irreflexivity_qorder` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbQ{}].  False  supposing  a  <  a


By

---

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

---

Home Index