---

Step * of Lemma stable__in-rat-cube

∀[k:ℕ]. ∀[p:ℝ^k]. ∀[c:ℚCube(k)].  Stable{in-rat-cube(k;p;c)}
BY
{ (Auto
   THEN RepUR ``in-rat-cube`` 0
   THEN Auto
   THEN (BLemma `stable__all` THEN Auto)
   THEN BLemma `stable__and`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[p:\mBbbR{}\^{}k].  \mforall{}[c:\mBbbQ{}Cube(k)].    Stable\{in-rat-cube(k;p;c)\}


By

---

Latex:
(Auto
  THEN  RepUR  ``in-rat-cube``  0
  THEN  Auto
  THEN  (BLemma  `stable\_\_all`  THEN  Auto)
  THEN  BLemma  `stable\_\_and`
  THEN  Auto)

---

Home Index