---

Step * of Lemma geo-strict-between-trans2

∀e:BasicGeometry-. ∀a,b,c,d:Point.  (d-a-b ⇒ d-b-c ⇒ a-b-c)
BY
{ (Auto THEN (InstLemma `geo-strict-between-trans` [⌜e⌝;⌜c⌝;⌜b⌝;⌜a⌝;⌜d⌝]⋅ THENA Auto) THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry-.  \mforall{}a,b,c,d:Point.    (d-a-b  {}\mRightarrow{}  d-b-c  {}\mRightarrow{}  a-b-c)


By

---

Latex:
(Auto  THEN  (InstLemma  `geo-strict-between-trans`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  EAuto  1)

---

Home Index