---

Step * of Lemma rat-sub-cube_transitivity

No Annotations
∀[k:ℕ]. ∀a,b,c:ℚCube(k).  (rat-sub-cube(k;a;b) ⇒ rat-sub-cube(k;b;c) ⇒ rat-sub-cube(k;a;c))
BY
{ (Auto
   THEN RepeatFor 2 (ParallelLast)
   THEN (D 5 With ⌜i⌝  THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜a i⌝;⌜b i⌝;⌜c i⌝]⋅
   THEN All Thin
   THEN D -2
   THEN D 1
   THEN D -1
   THEN RepUR ``rat-sub-interval`` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}].  \mforall{}a,b,c:\mBbbQ{}Cube(k).    (rat-sub-cube(k;a;b)  {}\mRightarrow{}  rat-sub-cube(k;b;c)  {}\mRightarrow{}  rat-sub-cube(k;a;c))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (D  5  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}a  i\mkleeneclose{};\mkleeneopen{}b  i\mkleeneclose{};\mkleeneopen{}c  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  D  -2
  THEN  D  1
  THEN  D  -1
  THEN  RepUR  ``rat-sub-interval``  0
  THEN  Auto)

---

Home Index