---

Step * of Lemma compatible-rat-cubes-refl

∀[k:ℕ]. ∀[c:ℚCube(k)].  ∀d:ℚCube(k). ((c = d ∈ ℚCube(k)) ⇒ Compatible(d;c))
BY
{ (Auto THEN D 0 THEN Auto THEN (RWO "-2" 0 THEN Auto) THEN RWO "rat-cube-intersection-idemp" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[c:\mBbbQ{}Cube(k)].    \mforall{}d:\mBbbQ{}Cube(k).  ((c  =  d)  {}\mRightarrow{}  Compatible(d;c))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (RWO  "-2"  0  THEN  Auto)
  THEN  RWO  "rat-cube-intersection-idemp"  0
  THEN  Auto)

---

Home Index