---

Step * of Lemma not-gt-2

∀x,y:ℤ.  uiff(¬(y > x);y ≤ x)
BY
{ (RepUR ``ge gt`` 0 THEN InstLemma `not-lt-2` [] THEN Hypothesis) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbZ{}.    uiff(\mneg{}(y  >  x);y  \mleq{}  x)


By

---

Latex:
(RepUR  ``ge  gt``  0  THEN  InstLemma  `not-lt-2`  []  THEN  Hypothesis)

---

Home Index