---

Step * of Lemma rless_irreflexivity

∀[e:ℝ]. False supposing e < e
BY
{ (Auto THEN InstLemma `rsub_functionality_wrt_rless` [⌜e⌝;⌜e⌝;⌜e⌝;⌜e⌝]⋅ THEN Auto THEN nRNorm (-1)) }

---

Latex:

---

Latex:
\mforall{}[e:\mBbbR{}].  False  supposing  e  <  e


By

---

Latex:
(Auto  THEN  InstLemma  `rsub\_functionality\_wrt\_rless`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  nRNorm  (-1))

---

Home Index