---

Step * of Lemma inhabited-rat-cube-face

∀[k:ℕ]. ∀[c:ℚCube(k)].  ((↑Inhabited(c)) ⇒ (∀f:ℚCube(k). (f ≤ c ⇒ (↑Inhabited(f)))))
BY
{ (Auto
   THEN UnfoldTopAb (-1)
   THEN (All (RWO "assert-inhabited-rat-cube") THENA Auto)
   THEN ParallelOp 3
   THEN (D -3 With ⌜i⌝  THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConclTerm ⌜c i⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN RepUR ``rat-interval-face`` 0
   THEN Auto
   THEN SplitOrHyps
   THEN Auto
   THEN RWO "-1" 0
   THEN Auto
   THEN RWO "inhabited-rat-point-interval" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[c:\mBbbQ{}Cube(k)].    ((\muparrow{}Inhabited(c))  {}\mRightarrow{}  (\mforall{}f:\mBbbQ{}Cube(k).  (f  \mleq{}  c  {}\mRightarrow{}  (\muparrow{}Inhabited(f)))))


By

---

Latex:
(Auto
  THEN  UnfoldTopAb  (-1)
  THEN  (All  (RWO  "assert-inhabited-rat-cube")  THENA  Auto)
  THEN  ParallelOp  3
  THEN  (D  -3  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConclTerm  \mkleeneopen{}c  i\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  RepUR  ``rat-interval-face``  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  RWO  "inhabited-rat-point-interval"  0
  THEN  Auto)

---

Home Index