---

Step * of Lemma member-rat-cube-faces

∀k:ℕ. ∀c:ℚCube(k).
  ∀f:ℚCube(k). ((f ∈ rat-cube-faces(k;c)) ⇐⇒ f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ)) supposing ↑Inhabited(c)
BY
{ ((UnivCD THENA Auto)
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN Try ((BLemma `implies-member-rat-cube-faces` THEN Auto))) }

1
1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
4. f : ℚCube(k)
5. (f ∈ rat-cube-faces(k;c))
⊢ f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}c:\mBbbQ{}Cube(k).
    \mforall{}f:\mBbbQ{}Cube(k).  ((f  \mmember{}  rat-cube-faces(k;c))  \mLeftarrow{}{}\mRightarrow{}  f  \mleq{}  c  \mwedge{}  (dim(f)  =  (dim(c)  -  1))) 
    supposing  \muparrow{}Inhabited(c)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  Try  ((BLemma  `implies-member-rat-cube-faces`  THEN  Auto)))

---

Home Index